diff --git a/Coq/syntax.v b/Coq/syntax.v index 780692fee34b521161bc052a5ebbb1fdaa2e6618..108e9ef9803714e5da0483130a51ade9d2801d43 100644 --- a/Coq/syntax.v +++ b/Coq/syntax.v @@ -1,7 +1,6 @@ (** Start to implement lambda pi modulo with pretty printing. TODO: - Have a better pretty printing for binders - - Have a pretty printer for application - no substitution - Try a localy nameless representation, but not implemented *) @@ -24,8 +23,9 @@ Inductive term : Set := Notation "'#' x" := (TFree x) (at level 10). Notation "'?' x" := (TBound x) (at level 10). -Notation "'Π' A '~' B" := (TPi A B) (at level 50). -Notation "'λ' A '~' B" := (TAbs A B) (at level 50). +Notation "'Π' A '~' B" := (TPi A B) (at level 45, right associativity). +Notation "'λ' A '~' u" := (TAbs A u) (at level 50). +Notation "t '@' u" := (TApp t u) (at level 50, left associativity). Definition of_sort (s:sort) : term := TSort s. Coercion of_sort : sort >-> term. @@ -54,6 +54,10 @@ Reserved Notation "Γ ✓" (at level 100). Inductive Conv (Γ: context) : term -> term -> Prop := . +Definition substk (t u : term) (k : nat) : term := t. (* TODO *) + +Notation "t '[' k '<-' u ']'" := (substk t u k) (at level 40, u at level 20). + Notation "Γ ⊧ t '≡' u" := (Conv Γ t u) (at level 50). Inductive typing : context -> term -> term -> Prop := @@ -62,7 +66,7 @@ Inductive typing : context -> term -> term -> Prop := | 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 -> Γ ⊢ TApp t u : 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 :=