Commit 7d61aa26 authored by François Thiré's avatar François Thiré

Fix typing with LN

parent 6132d9f5
......@@ -6,7 +6,7 @@
*)
Require Import PeanoNat.
Require Import List.
Parameter Var : Set.
Axiom var_dec : forall (x y:Var), {x = y} + {x <> y}.
......@@ -122,10 +122,15 @@ Notation "Γ ⊧ t '≡' u" := (Conv Γ t u).
Inductive typing : context -> term -> term -> Prop :=
| TyAxiom : forall Γ x A, Γ -> x : A Γ -> Γ (# x) : A
| TyType : forall Γ, Γ -> Γ type : kind
| TyPi : forall Γ A B s x, Γ A : type -> Γ, x : A B : s -> Γ Π A ~ B : s
| TyAbs : forall Γ x A B t s, Γ A : type -> Γ, x : A B : s -> Γ, x : A t : B -> Γ λ A ~ t : Π A ~ B
| TyApp : forall Γ t u A B, Γ t : Π A ~ B -> Γ u : A -> Γ t @ u : B [0 <- u]
| TyConv : forall Γ t A B s, Γ t : A -> Γ B : s -> Γ A B -> Γ t : B
| TyPi : forall Γ A B s L,
Γ A : type ->
(forall x, ~(In x L) -> Γ, x : A B : s) -> Γ Π A ~ B : s
| TyAbs : forall Γ A B t s L,
Γ A : type ->
(forall x, ~ (In x L) -> Γ, x : A B : s) ->
(forall x, ~ (In x L) -> Γ, x : A t : B) -> Γ λ A ~ t : Π A ~ B
| TyApp : forall Γ t u A B, Γ t : Π A ~ B -> Γ u : A -> Γ t @ u : B [0 <- u]
| TyConv : forall Γ t A B s, Γ t : A -> Γ B : s -> Γ A B -> Γ t : B
where "Γ '⊢' t ':' A" := (typing Γ t A)
with well_formed : context -> Prop :=
| WFEmpty : [ ]
......
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