this repo has no description
initial commit
+163
+1
.gitignore
+1
.gitignore
···
1
+
/build
+155
Learn-lean/DepType.lean
+155
Learn-lean/DepType.lean
···
1
+
namespace Intro
2
+
3
+
/-
4
+
Lean natural numbers are arbitrary precision unsigned integers.
5
+
Type is an abbrev. for Type 0 (universe of types)
6
+
-/
7
+
8
+
constant a : Nat
9
+
constant b : Nat
10
+
11
+
constant f : Nat → Nat
12
+
constant t: Nat × Nat
13
+
constant T: Prod Nat Nat
14
+
constant F: (Nat -> Nat) -> Nat
15
+
16
+
#check a
17
+
#check a + 4
18
+
#check f
19
+
#check t.1
20
+
#check T.fst
21
+
#check F f
22
+
23
+
#check Nat
24
+
#check Nat -> Bool
25
+
26
+
constant α : Type
27
+
constant 𝔽 : Type -> Type
28
+
29
+
#check 𝔽 α
30
+
#check 𝔽 Bool
31
+
#check Prod α Nat
32
+
33
+
#check Type
34
+
#check List
35
+
#check Prod
36
+
37
+
constant C : Type _
38
+
universe U
39
+
constant D : Type U
40
+
#check C
41
+
#check D
42
+
43
+
-- fn :: a -> a
44
+
-- fn a = a
45
+
def fn (α : Type _)(a : α) := a
46
+
#check fn
47
+
end Intro
48
+
49
+
namespace Fun_Abstraction
50
+
51
+
#check fun (x: Nat) => x + 5
52
+
#check λ (α : Type _) (a: α) => a
53
+
54
+
constant f : Nat -> Bool -> Bool
55
+
constant h : Nat -> Bool
56
+
#check fun x y => f x (h y)
57
+
58
+
/-alpha equivalence-/
59
+
constant b: Bool
60
+
#check (fun (α β : Type) (b: β) (x: α) => b) Nat Bool
61
+
#reduce (fun (α β : Type) (b: β) (x: α) => b) Nat Bool
62
+
end Fun_Abstraction
63
+
64
+
/-definitions-/
65
+
constant Bar : Nat -> Nat -> Nat
66
+
constant x : Nat
67
+
constant y : Nat
68
+
def bar (x : Nat) (y : Nat) : Nat := x + y
69
+
70
+
/-this approach of defining functions is better-/
71
+
def barr : Nat -> Nat -> Nat :=
72
+
fun x y => x + y
73
+
74
+
#check Bar
75
+
#check Bar x y
76
+
#reduce Bar x y
77
+
#check bar
78
+
#print bar
79
+
#eval bar 1 2
80
+
#reduce bar
81
+
82
+
#check barr
83
+
#reduce barr
84
+
#eval barr 2 3
85
+
#print barr
86
+
87
+
def f (α : Type u) (β : α -> Type v) (a : α) (b: β a) : (a : α) × β a := ⟨ a, b ⟩
88
+
89
+
#reduce f
90
+
#reduce (f Type (fun α => α) Nat 10).2
91
+
92
+
section
93
+
variable (α β γ : Type)
94
+
variable (g: β -> γ) (f: α -> β) (h: α -> α)
95
+
variable (x: α)
96
+
97
+
def compose := g (f x)
98
+
def doTwice := h (h x)
99
+
def doThrice := h (h (h x))
100
+
101
+
#print compose
102
+
#print doTwice
103
+
#print doThrice
104
+
end
105
+
106
+
namespace typeclasses
107
+
108
+
class Add(α : Type) where
109
+
add : α → α → α
110
+
111
+
#check @Add.add
112
+
113
+
constant el : Type u -> Type u
114
+
namespace el
115
+
universe u
116
+
117
+
inductive nat: Type u where
118
+
| z : nat
119
+
| succ : nat -> nat
120
+
121
+
#check nat.succ nat.z
122
+
123
+
def add (a: nat) (b: nat): nat :=
124
+
match a with
125
+
| nat.z => b
126
+
| nat.succ x => nat.succ (add x b)
127
+
128
+
#reduce add (nat.succ nat.z) (nat.succ nat.z)
129
+
130
+
constant F : { a : Type u } -> List a -> Type u
131
+
132
+
constant a : Type v
133
+
def b := List (List (Type u))
134
+
#check b
135
+
#check F
136
+
#check F List.nil
137
+
138
+
universe v
139
+
inductive elof (α : Type v): Type v where
140
+
| mk (a : α) : elof α
141
+
142
+
def elof.mk1 : {α : Type u} -> { n: List α } -> (b : List (List α)) -> elof (List α) :=
143
+
fun {α} {n} xs => match xs with
144
+
| List.nil => elof.mk n
145
+
| List.cons _ => elof.mk n
146
+
| List.cons (List.cons a List.nil) _ => elof.mk n
147
+
148
+
-- #check @elof.mk a
149
+
-- #check List.cons
150
+
-- #reduce elof.mk1 (List.cons a List.nil : List (Type v))
151
+
-- #reduce elof.mk1 (List.nil : List (Type v))
152
+
153
+
end el
154
+
155
+
end typeclasses