Commit 420ba9fc authored by François Thiré's avatar François Thiré

add notation for applications

parent a6bba167
(** Start to implement lambda pi modulo with pretty printing. (** Start to implement lambda pi modulo with pretty printing.
TODO: TODO:
- Have a better pretty printing for binders - Have a better pretty printing for binders
- Have a pretty printer for application
- no substitution - no substitution
- Try a localy nameless representation, but not implemented - Try a localy nameless representation, but not implemented
*) *)
...@@ -24,8 +23,9 @@ Inductive term : Set := ...@@ -24,8 +23,9 @@ Inductive term : Set :=
Notation "'#' x" := (TFree x) (at level 10). Notation "'#' x" := (TFree x) (at level 10).
Notation "'?' x" := (TBound x) (at level 10). Notation "'?' x" := (TBound x) (at level 10).
Notation "'Π' A '~' B" := (TPi A B) (at level 50). Notation "'Π' A '~' B" := (TPi A B) (at level 45, right associativity).
Notation "'λ' A '~' B" := (TAbs A B) (at level 50). 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. Definition of_sort (s:sort) : term := TSort s.
Coercion of_sort : sort >-> term. Coercion of_sort : sort >-> term.
...@@ -54,6 +54,10 @@ Reserved Notation "Γ ✓" (at level 100). ...@@ -54,6 +54,10 @@ Reserved Notation "Γ ✓" (at level 100).
Inductive Conv (Γ: context) : term -> term -> Prop := . 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). Notation "Γ ⊧ t '≡' u" := (Conv Γ t u) (at level 50).
Inductive typing : context -> term -> term -> Prop := Inductive typing : context -> term -> term -> Prop :=
...@@ -62,7 +66,7 @@ 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 | 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 -> | TyAbs : forall Γ x A B t s, Γ A : type -> Γ, x : A B : s ->
Γ, x : A t : B -> Γ λ A ~ t : Π A ~ B Γ, 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 | TyConv : forall Γ t A B s, Γ t : A -> Γ B : s -> Γ A B -> Γ t : B
where "Γ '⊢' t ':' A" := (typing Γ t A) where "Γ '⊢' t ':' A" := (typing Γ t A)
with well_formed : context -> Prop := with well_formed : context -> Prop :=
......
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