Commit 00b260cc authored by Gaspard Ferey's avatar Gaspard Ferey

Fixed .gitignore. Added STT.

parent 78ab7ede
......@@ -21,8 +21,8 @@
*.mtc1
*.out
*.synctex.gz
.vo
.glob
*.vo
*.glob
*~
\#*\#
......
Require Import LPTerm.
Parameter type : Var.
Parameter ι : Var.
Parameter o : Var.
Parameter arrow : Var.
Parameter η : Var.
Parameter impl : Var.
Parameter pi : Var.
Parameter ϵ : Var.
Definition STT :=
[],
type : TType,
ι : # type,
o : # type,
arrow : Π (# type) ~ Π (# type) ~ (# type),
η : Π (# type) ~ TType,
impl : Π (TApp (# η) (# o)) ~ Π (TApp (# η) (# o)) ~ (TApp (# η) (# o)),
pi :
Π (# type) ~ Π (Π (TApp (# η) (TBound 0)) ~ (TApp (# η) (# o))) ~ (TApp (# η) (# o))
(* TODO *)
.
Theorem STT_WF : STT .
Proof.
Admitted.
Require Import LPTerm.
Lemma no_type_kind : forall Γ A, Γ kind : A -> False.
Proof.
intros.
......@@ -96,3 +93,5 @@ Proof.
- eapply CVTrans ; [eapply IHRSTClosure1 | eapply IHRSTClosure2] ; easy.
- eapply CVRule ; eapply context_var_conv_βΓ ; now rewrite <- HeqΓ0.
Qed.
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