diff options
author | Jason Gross <jgross@mit.edu> | 2016-11-16 14:38:00 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-11-16 14:38:00 -0500 |
commit | cb2a844448f42bf65f33f885a5018d11bebb68d6 (patch) | |
tree | b917583627e7089411646712bf33ede7858430c2 /src/Reflection/Syntax.v | |
parent | 804189588135ba5e35f4fc4287f12b4179653620 (diff) |
Add : assert to a bunch of arguments
Diffstat (limited to 'src/Reflection/Syntax.v')
-rw-r--r-- | src/Reflection/Syntax.v | 90 |
1 files changed, 45 insertions, 45 deletions
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index 54336861d..00a176428 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -383,11 +383,11 @@ Section language. Axiom Wf_admitted : forall {t} (E:Expr t), @Wf t E. End expr_param. End language. -Global Arguments tuple' {_}%type_scope _%ctype_scope _%nat_scope. -Global Arguments tuple {_}%type_scope _%ctype_scope _%nat_scope. -Global Arguments Prod {_}%type_scope (_ _)%ctype_scope. -Global Arguments Arrow {_}%type_scope (_ _)%ctype_scope. -Global Arguments Tbase {_}%type_scope _%ctype_scope. +Global Arguments tuple' {_}%type_scope _%ctype_scope _%nat_scope : assert. +Global Arguments tuple {_}%type_scope _%ctype_scope _%nat_scope : assert. +Global Arguments Prod {_}%type_scope (_ _)%ctype_scope : assert. +Global Arguments Arrow {_}%type_scope (_ _)%ctype_scope : assert. +Global Arguments Tbase {_}%type_scope _%ctype_scope : assert. Ltac admit_Wf := apply Wf_admitted. @@ -405,46 +405,46 @@ Proof. repeat intro; hnf; decide equality; apply dec; typeclasses eauto. Defined. -Global Arguments Const {_ _ _ _ _} _. -Global Arguments Var {_ _ _ _ _} _. -Global Arguments SmartVarf {_ _ _ _ _} _. -Global Arguments SmartValf {_} T _ t. -Global Arguments SmartVarVarf {_ _ _ _ _} _. -Global Arguments SmartVarfMap {_ _ _} _ {_} _. -Global Arguments SmartVarMap_hetero {_ _ _ _ _} _ _ {_} _. -Global Arguments SmartVarMap {_ _ _} _ _ {_} _. -Global Arguments SmartConstf {_ _ _ _ _} _. -Global Arguments Op {_ _ _ _ _ _} _ _. -Global Arguments LetIn {_ _ _ _ _} _ {_} _. -Global Arguments Pair {_ _ _ _ _} _ {_} _. -Global Arguments Return {_ _ _ _ _} _. -Global Arguments Abs {_ _ _ _ _ _} _. -Global Arguments SmartAbs {_ _ _ _ _ _} _. -Global Arguments UnReturn {_ _ _ _ _} _. -Global Arguments UnAbs {_ _ _ _ _ _} _. -Global Arguments flat_interp_tuple' {_ _ _ _} _. -Global Arguments flat_interp_tuple {_ _ _ _} _. -Global Arguments flat_interp_untuple' {_ _ _ _} _. -Global Arguments interp_type_rel_pointwise2 {_ _ _} R {t} _ _. -Global Arguments interp_type_gen_rel_pointwise2_hetero {_ _ _ _ _} Rsrc R {t} _ _. -Global Arguments interp_type_gen_rel_pointwise2 {_ _ _} R {t} _ _. -Global Arguments interp_flat_type_rel_pointwise2_gen_Prop {_ _ _ P} and R {t} _ _. -Global Arguments interp_flat_type_rel_pointwise2 {_ _ _} R {t} _ _. -Global Arguments mapf_interp_flat_type {_ _ _} _ {t} _. -Global Arguments interp_type_gen_hetero {_} _ _ _. -Global Arguments interp_type_gen {_} _ _. -Global Arguments interp_flat_type {_} _ _. -Global Arguments interp_type_rel_pointwise {_} _ _ {_} _ _. -Global Arguments interp_type_gen_rel_pointwise {_ _} _ {_} _ _. -Global Arguments interp_flat_type_rel_pointwise {_} _ _ {_} _ _. -Global Arguments interp_type {_} _ _. -Global Arguments wff {_ _ _ _ _} G {t} _ _. -Global Arguments wf {_ _ _ _ _} G {t} _ _. -Global Arguments Wf {_ _ _ t} _. -Global Arguments Interp {_ _ _} interp_op {t} _. -Global Arguments interp {_ _ _} interp_op {t} _. -Global Arguments interpf {_ _ _} interp_op {t} _. -Global Arguments invert_Const {_ _ _ _ _} _. +Global Arguments Const {_ _ _ _ _} _ : assert. +Global Arguments Var {_ _ _ _ _} _ : assert. +Global Arguments SmartVarf {_ _ _ _ _} _ : assert. +Global Arguments SmartValf {_} T _ t : assert. +Global Arguments SmartVarVarf {_ _ _ _ _} _ : assert. +Global Arguments SmartVarfMap {_ _ _} _ {_} _ : assert. +Global Arguments SmartVarMap_hetero {_ _ _ _ _} _ _ {_} _ : assert. +Global Arguments SmartVarMap {_ _ _} _ _ {_} _ : assert. +Global Arguments SmartConstf {_ _ _ _ _} _ : assert. +Global Arguments Op {_ _ _ _ _ _} _ _ : assert. +Global Arguments LetIn {_ _ _ _ _} _ {_} _ : assert. +Global Arguments Pair {_ _ _ _ _} _ {_} _ : assert. +Global Arguments Return {_ _ _ _ _} _ : assert. +Global Arguments Abs {_ _ _ _ _ _} _ : assert. +Global Arguments SmartAbs {_ _ _ _ _ _} _ : assert. +Global Arguments UnReturn {_ _ _ _ _} _ : assert. +Global Arguments UnAbs {_ _ _ _ _ _} _ _ : assert. +Global Arguments flat_interp_tuple' {_ _ _ _} _ : assert. +Global Arguments flat_interp_tuple {_ _ _ _} _ : assert. +Global Arguments flat_interp_untuple' {_ _ _ _} _ : assert. +Global Arguments interp_type_rel_pointwise2 {_ _ _} R {t} _ _ : assert. +Global Arguments interp_type_gen_rel_pointwise2_hetero {_ _ _ _ _} Rsrc R {t} _ _ : assert. +Global Arguments interp_type_gen_rel_pointwise2 {_ _ _} R {t} _ _ : assert. +Global Arguments interp_flat_type_rel_pointwise2_gen_Prop {_ _ _ P} and R {t} _ _ : assert. +Global Arguments interp_flat_type_rel_pointwise2 {_ _ _} R {t} _ _ : assert. +Global Arguments mapf_interp_flat_type {_ _ _} _ {t} _ : assert. +Global Arguments interp_type_gen_hetero {_} _ _ _ : assert. +Global Arguments interp_type_gen {_} _ _ : assert. +Global Arguments interp_flat_type {_} _ _ : assert. +Global Arguments interp_type_rel_pointwise {_} _ _ {_} _ _ : assert. +Global Arguments interp_type_gen_rel_pointwise {_ _} _ {_} _ _ : assert. +Global Arguments interp_flat_type_rel_pointwise {_} _ _ {_} _ _ : assert. +Global Arguments interp_type {_} _ _ : assert. +Global Arguments wff {_ _ _ _ _} G {t} _ _ : assert. +Global Arguments wf {_ _ _ _ _} G {t} _ _ : assert. +Global Arguments Wf {_ _ _ t} _ : assert. +Global Arguments Interp {_ _ _} interp_op {t} _ : assert. +Global Arguments interp {_ _ _} interp_op {t} _ : assert. +Global Arguments interpf {_ _ _} interp_op {t} _ : assert. +Global Arguments invert_Const {_ _ _ _ _} _ : assert. Module Export Notations. Notation "A * B" := (@Prod _ A B) : ctype_scope. |