diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-27 14:14:31 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-27 14:14:31 -0400 |
| commit | 81079fb8bb3ca331cf146aa12c6ecf1e92f7d2ab (patch) | |
| tree | f13b399894a807449bf7a2cc1ce72bbc653a0363 /src/Reflection/Syntax.v | |
| parent | 72af7655d9227fcba3949a2a9d9e39d5116a568a (diff) | |
PHOAS notation fixups
Diffstat (limited to 'src/Reflection/Syntax.v')
| -rw-r--r-- | src/Reflection/Syntax.v | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index af6ab3e20..43405fbbd 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -238,11 +238,9 @@ Section language. Axiom Wf_admitted : forall {t} (E:Expr t), @Wf t E. End expr_param. End language. -Global Arguments Prod {_} _ _. -Global Arguments Arrow {_} _ _. -Global Arguments Tbase {_} _. -Infix "*" := (@Prod _) : ctype_scope. -Notation "A -> B" := (@Arrow _ A B) : ctype_scope. +Global Arguments Prod {_}%type_scope (_ _)%ctype_scope. +Global Arguments Arrow {_}%type_scope (_ _)%ctype_scope. +Global Arguments Tbase {_}%type_scope _%ctype_scope. Ltac admit_Wf := apply Wf_admitted. @@ -274,7 +272,11 @@ Global Arguments interpf {_ _ _} interp_op {t} _. Global Arguments invert_Const {_ _ _ _ _} _. Module Export Notations. + Notation "A * B" := (@Prod _ A B) : ctype_scope. + Notation "A -> B" := (@Arrow _ A B) : ctype_scope. Notation "'slet' x := A 'in' b" := (LetIn A (fun x => b)) : expr_scope. Notation "'λ' x .. y , t" := (Abs (fun x => .. (Abs (fun y => t%expr)) ..)) : expr_scope. Notation "( x , y , .. , z )" := (Pair .. (Pair x%expr y%expr) .. z%expr) : expr_scope. + Bind Scope ctype_scope with flat_type. + Bind Scope ctype_scope with type. End Notations. |