Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits: 46381fd8 by Jonathan Graveline at 2018-06-25T18:11:36Z samples/list_n.typer, there must be some mistakes
- - - - -
1 changed file:
- + samples/list_n.typer
Changes:
===================================== samples/list_n.typer ===================================== @@ -0,0 +1,37 @@ +%%% +%%% Size proved list : n_list +%%% + +Nat : Type; + +type Nat + | zero + | succ Nat; + +Nat_add : Nat -> Nat -> Nat; + +Nat_add n k = case n + | (succ n) => Nat_add n (succ k) + | zero => k; + +Nat_eq : Nat -> Nat -> Type; +Nat_eq n k = case (n,k) + | (succ n,succ k) => Nat_eq n k + | (zero,zero) => True + | False; + +one = succ zero; + +List_n : Nat -> Type -> Type; + +type List_n (n : Nat) (a : Type) + | cons a (List_n sn a) (p ::: (Nat_eq n (succ sn))) + | nil (p ::: (Nat_eq n zero)); + +len : (n : Nat) ≡> (a : Type) ≡> List_n n a -> Nat; +len xs = case (xs) + | cons x xs => succ (len xs) + | nil => zero; + +%prep : (n : Nat) ≡> a -> List_n n a -> List_n (succ n) a; +%prep x xs = cons (n := (succ n)) x xs (Nat_eq (succ n) (succ n));
View it on GitLab: https://gitlab.com/monnier/typer/commit/46381fd83e2e2651d52d0aa645712b57a0cd...