diff options
| -rw-r--r-- | plastic/test.lf | 64 |
1 files changed, 0 insertions, 64 deletions
diff --git a/plastic/test.lf b/plastic/test.lf deleted file mode 100644 index 7c163d3d..00000000 --- a/plastic/test.lf +++ /dev/null @@ -1,64 +0,0 @@ -EXAMPLE FILE: less than or equal on Nat - -%--------------------------------------- -Nat - -> Inductive -> [Nat : Type] -> Constructors -> [zero : Nat] -> [succ : (n:Nat)Nat]; - -> [plus [m:Nat] = E_Nat ([_:Nat]Nat) m ([_:Nat]succ) ]; - - ------------------------ -Non-dependent Pi type. - -> Inductive -> [A,B:Type] -> [Pi_ : Type] -> Constructors -> [La_ : (f:(x:El A)El B)Pi_ ]; - - -application of Pi_ types, ie conversion to a dependent product. - -> Claim ap_ : (A,B:Type) Pi_ A B -> A -> B; -> Intros A B f x; -> Refine E_Pi_ ? ? ([_:?]B); -> Refine f; -> Intros fo; -> Refine fo x; -> ReturnAll; -> ap_; - - - -%--------------------------------------- -Combined leq with if-branch - thus avoiding Boolean type. - -Notice that we have to prove (Pi_ Nat T) by induction on x, since we can't -eliminate over (Nat -> T) in LF. - - -> Claim if_leq : (x,y:Nat)(T:Type)T -> T -> T; -> Intros x y T leq not_leq; -> Refine ap_ ? ? (ap_ ? ? ? x) y; - -> Refine La_; -> Intros x1; -> Refine E_Nat ([_:?]Pi_ Nat T) ?x_z ?x_s x1; -> x_z Refine La_ ? ? ([_:?]leq); -> Intros x1_ f_x1_; -> Refine La_; -> Intros y1; -> Refine E_Nat ([_:?]T) ?y_z ?y_s y1; -> y_z Refine not_leq; -> Intros y1_ _; -> Refine ap_ ? ? f_x1_ y1_; -> ReturnAll; - -> if_leq; - - |