Commit 75ccb503 authored by François Thiré's avatar François Thiré

Having a Parser for lFMT would be a good idea

parent 00b260cc
...@@ -8,8 +8,8 @@ Parameter o : Var. ...@@ -8,8 +8,8 @@ Parameter o : Var.
Parameter arrow : Var. Parameter arrow : Var.
Parameter η : Var. Parameter η : Var.
Parameter impl : Var. Parameter impl : Var.
Parameter pi : Var. Parameter fa : Var.
Parameter ϵ : Var. Parameter ε : Var.
Definition STT := Definition STT :=
...@@ -19,13 +19,14 @@ Definition STT := ...@@ -19,13 +19,14 @@ Definition STT :=
o : # type, o : # type,
arrow : Π (# type) ~ Π (# type) ~ (# type), arrow : Π (# type) ~ Π (# type) ~ (# type),
η : Π (# type) ~ TType, η : Π (# type) ~ TType,
ε : Π ((# η) @ (# o)) ~ ((# η) @ (# o)),
impl : Π (TApp (# η) (# o)) ~ Π (TApp (# η) (# o)) ~ (TApp (# η) (# o)), impl : Π (TApp (# η) (# o)) ~ Π (TApp (# η) (# o)) ~ (TApp (# η) (# o)),
pi : fa :
Π (# type) ~ Π (Π (TApp (# η) (TBound 0)) ~ (TApp (# η) (# o))) ~ (TApp (# η) (# o)) Π (# type) ~ Π (Π (TApp (# η) (TBound 0)) ~ (TApp (# η) (# o))) ~ (TApp (# η) (# o)),
(* TODO *) λ (# type) ~ (λ (# type) ~ (# η) @ ((# arrow) @ (? 0) @ (? 1))) λ (# type) ~ (λ (# type) ~ (Π ((# η) @ (? 0)) ~ (# η) @ (? 1)))
. .
Theorem STT_WF : STT . Theorem STT_WF : STT .
Proof. Proof.
Admitted. Admitted.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment