Skip to content

Commit

Permalink
Add vector example
Browse files Browse the repository at this point in the history
  • Loading branch information
Ailrun committed Sep 5, 2024
1 parent 7c2a1b3 commit af5db8e
Show file tree
Hide file tree
Showing 2 changed files with 62 additions and 9 deletions.
30 changes: 21 additions & 9 deletions examples/pair.mltt
Original file line number Diff line number Diff line change
@@ -1,11 +1,23 @@
(
(fun (Pair : forall (A : Type@0) (B : Type@0) -> Type@1)
(fst : forall (A : Type@0) (B : Type@0) (p : Pair A B) -> A)
(snd : forall (A : Type@0) (B : Type@0) (p : Pair A B) -> B)
(p : Pair Nat (forall (x : Nat) -> Nat)) ->
snd Nat (forall (x : Nat) -> Nat) p (fst Nat (forall (x : Nat) -> Nat) p))
(fun (A : Type@0) (B : Type@0) -> forall (C : Type@0) (cons : forall (a : A) (b : B) -> C) -> C)
(fun (A : Type@0) (B : Type@0) (p : forall (C : Type@0) (cons : forall (a : A) (b : B) -> C) -> C) -> p A (fun (a : A) (b : B) -> a))
(fun (A : Type@0) (B : Type@0) (p : forall (C : Type@0) (cons : forall (a : A) (b : B) -> C) -> C) -> p B (fun (a : A) (b : B) -> b))
(fun (C : Type@0) (cons : forall (a : Nat) (b : forall (x : Nat) -> Nat) -> C) -> cons 3 (fun (x : Nat) -> succ x))
(* Main example *)
(
fun (Pair : forall (A : Type@0) (B : Type@0) -> Type@1)
(pair : forall (A : Type@0) (B : Type@0) (a : A) (b : B) -> Pair A B)
(fst : forall (A : Type@0) (B : Type@0) (p : Pair A B) -> A)
(snd : forall (A : Type@0) (B : Type@0) (p : Pair A B) -> B) ->
(
fun (p : Pair Nat (forall (x : Nat) -> Nat)) ->
snd Nat (forall (x : Nat) -> Nat) p
(fst Nat (forall (x : Nat) -> Nat) p)
)
(pair Nat (forall (x : Nat) -> Nat) 3 (fun (x : Nat) -> succ (succ x)))
)
(* Church pair *)
(fun (A : Type@0) (B : Type@0) -> forall (C : Type@0) (pair : forall (a : A) (b : B) -> C) -> C)
(* Church pair constructor *)
(fun (A : Type@0) (B : Type@0) (a : A) (b : B) (C : Type@0) (pair : forall (a : A) (b : B) -> C) -> pair a b)
(* Church pair fst *)
(fun (A : Type@0) (B : Type@0) (p : forall (C : Type@0) (pair : forall (a : A) (b : B) -> C) -> C) -> p A (fun (a : A) (b : B) -> a))
(* Church pair snd *)
(fun (A : Type@0) (B : Type@0) (p : forall (C : Type@0) (pair : forall (a : A) (b : B) -> C) -> C) -> p B (fun (a : A) (b : B) -> b))
) : Nat
41 changes: 41 additions & 0 deletions examples/vector.mltt
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
(
(* Main example *)
(
fun (Vec : forall (A : Type@0) (n : Nat) -> Type@2)
(nil : forall (A : Type@0) -> Vec A 0)
(cons : forall (A : Type@0) (n : Nat) (head : A) (tail : Vec A n) -> Vec A (succ n))
(vecRec : forall (A : Type@0) (n : Nat) (vec : Vec A n) (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> C n) ->
(
fun (totalHead : forall (A : Type@0) (n : Nat) (vec : Vec A (succ n)) -> A)
(vec : Vec (forall (n : Nat) -> Nat) 3) ->
totalHead ((forall (n : Nat) -> Nat)) 2 vec 4
)
(* total head function *)
(
fun (A : Type@0) (n : Nat) (vec : Vec A (succ n)) ->
vecRec A (succ n) vec (fun (l : Nat) -> rec l return r -> Type@0 | zero => Nat | succ l, r => A end) 0 (fun (l : Nat) (a : A) (r : rec l return r -> Type@0 | zero => Nat | succ l, r => A end) -> a)
)
(* example vector *)
(
cons (forall (n : Nat) -> Nat) 2
(fun (n : Nat) -> succ (succ (succ n)))
(
cons (forall (n : Nat) -> Nat) 1
(fun (n : Nat) -> succ n)
(
cons (forall (n : Nat) -> Nat) 0
(fun (n : Nat) -> succ (succ n))
(nil (forall (n : Nat) -> Nat))
)
)
)
)
(* Church vector *)
(fun (A : Type@0) (n : Nat) -> forall (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> C n)
(* Church vector nil *)
(fun (A : Type@0) (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> nil)
(* Church vector cons *)
(fun (A : Type@0) (n : Nat) (head : A) (tail : forall (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> C n) (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> cons n head (tail C nil cons))
(* Church vector recursor *)
(fun (A : Type@0) (n : Nat) (vec : forall (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> C n) (C : forall (l : Nat) -> Type@1) (nil : C 0) (cons : forall (l : Nat) (a : A) (r : C l) -> C (succ l)) -> vec C nil cons)
) : Nat

0 comments on commit af5db8e

Please sign in to comment.