diff options
| author |  Jason Gross <jagro@google.com> | 2016-09-05 20:13:08 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-09-05 20:13:08 -0700 |
| commit | 0f9283bbca9acac6f927ba1dd47806b57e95f89e (patch) | |
| tree | ed5b7c4e91f3cc12d04cdcb5939b15e7d0c0ecc1 /src | |
| parent | 29a462c0cb69af343e28b205628115354cd573ad (diff) | |
Better implicits for interp
Diffstat (limited to 'src')
| -rw-r--r-- | src/Reflection/Syntax.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index ae4cbb6e2..71d7e49f1 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -206,6 +206,7 @@ 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} _. Notation "'slet' x := A 'in' b" := (Let A (fun x => b)) : expr_scope. Notation "'λ' x .. y , t" := (Abs (fun x => .. (Abs (fun y => t%expr)) ..)) : expr_scope. |