-
Notifications
You must be signed in to change notification settings - Fork 0
/
Prelude.zu
44 lines (37 loc) · 1.08 KB
/
Prelude.zu
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
module Prelude
/// | Defines inductive type for Leibniz equality and
/// reflection.
///
/// Performs unification and by unification, it proves
/// some value
@[alias `:=]
inductive data Eq of {a}, x, y : a where
| Refl : {a} -> {x : a} -> Eq x x
/// | Defines a proof that, `a := b` and `b := c` implies
/// `a := c`.
fun Eq/trans : {a, b, c} -> (a := b) -> (b := c) -> (a := c)
/// | Defines a proof that: `a = b`, implies `b = a` by
/// induction.
fun Eq/symm : {a, b} -> (a := b) -> (b := a)
/// | Represents a type of a dependent pair.
@[alias `$]
record Sigma of x, f : * -> * where
val inf : x
val ins : f a
/// | Record for lazy evaluation
@[do_notation IO/pure, IO/apply]
fun IO : Type -> Type
fun IO/pure : {a} -> a -> IO a
fun IO/apply : {a, b} -> IO a -> (IO a -> IO b) -> IO b
/// | Prints in the stdout
///
/// ```
/// main : IO () := do
/// println "hello world"
/// ```
fun println : String -> IO Unit
/// | Performs unsafe IO in the type level, or anywhere you are.
///
/// It's unsafe and should not be used.
@[partial]
fun unsafePerformIO : {a} -> IO a -> a