111 lines
1.9 KiB
Plaintext
111 lines
1.9 KiB
Plaintext
/- "Hello" -/
|
||
#eval "hello" ++ " " ++ "world"
|
||
|
||
#check true
|
||
|
||
def x := 10
|
||
|
||
#eval x + 2
|
||
|
||
def double (x:Int) := 2*x
|
||
|
||
#eval double 3
|
||
|
||
#check double
|
||
|
||
example: double 4 = 8 := rfl
|
||
|
||
#check rfl
|
||
|
||
/- First class functions -/
|
||
|
||
def twice (f:Nat -> Nat) (a:Nat) := f (f a)
|
||
#eval twice (fun x=>x+2) 3
|
||
|
||
theorem twice_add_2 (a:Nat) : twice (fun x=>x+2) a = a +4 := rfl
|
||
|
||
-- `(. + 2)` is fun x => x+2
|
||
|
||
#eval twice (fun x=>x+2) 10
|
||
|
||
/- Enum types -/
|
||
inductive Weekday where
|
||
| sunday | monday | tuesday
|
||
|
||
#check Weekday.sunday
|
||
|
||
|
||
-- open namespace
|
||
open Weekday
|
||
#check sunday
|
||
|
||
def natOfWeekday (d:Weekday):Nat:=
|
||
match d with
|
||
| sunday => 1
|
||
| monday => 2
|
||
| tuesday => 3
|
||
|
||
def Weekday.next (d:Weekday) : Weekday :=
|
||
match d with
|
||
| sunday => monday
|
||
| monday => tuesday
|
||
| tuesday => sunday
|
||
|
||
def Weekday.previous : Weekday -> Weekday
|
||
| sunday => tuesday
|
||
| monday => sunday
|
||
| tuesday => monday
|
||
|
||
theorem Weekday.next_previous (d:Weekday) : d.next.previous = d :=
|
||
match d with
|
||
| sunday => rfl -- reflexivity
|
||
| monday => rfl
|
||
| tuesday => rfl
|
||
|
||
-- tactics
|
||
theorem Weekday.next_previous' (d:Weekday) : d.next.previous = d := by
|
||
cases d -- makes 7 goals
|
||
rfl; rfl; rfl
|
||
|
||
theorem Weekday.next_previous'' (d:Weekday) : d.next.previous = d := by
|
||
cases d <;> rfl -- combinator apply
|
||
|
||
/- next -/
|
||
-- type hierarchy to avoid inconsistency
|
||
#check 0 -- Nat
|
||
#check Nat
|
||
#check Type
|
||
#check Type 1
|
||
|
||
#check Eq.refl 2
|
||
|
||
#check Prop
|
||
|
||
-- universes
|
||
example : Prop = Sort 0 := rfl
|
||
example : Type = Sort 1 := rfl
|
||
example : Type 1 = Sort 2 := rfl
|
||
|
||
/- polymorphism -/
|
||
def f (α β:Sort u)(a:α) (b:β) : α := a
|
||
#eval f Nat String 1 "hello"
|
||
|
||
-- implicit args
|
||
def g {α β:Sort u} (a:α)(b:β):α := a
|
||
#eval g 1 "hello"
|
||
|
||
def h (a:α)(b:β):α := a
|
||
|
||
#check g
|
||
#check @g
|
||
#check @h
|
||
#check g (α:=Nat) (β:=String)
|
||
/-
|
||
g : ?m.1377 → ?m.1378 → ?m.1377
|
||
@g : {α β : Sort u_1} → α → β → α
|
||
@h : {α : Sort u_1} → {β : Sort u_2} → α → β → α
|
||
g : Nat → String → Nat
|
||
-/
|
||
|
||
|