pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2025-02-26 03:22:13 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Revising Interpreters before class

Browse source
This commit is contained in:
Adam Chlipala 2020-02-09 14:50:46 -05:00
parent c050ec21ae
commit 56af55f38a
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
Interpreters_template.v
View file

@ -249,6 +249,7 @@ Example factorial_ugly :=
* them from our examples. *) * them from our examples. *)
Coercion Const : nat >-> arith. Coercion Const : nat >-> arith.
Coercion Var : var >-> arith. Coercion Var : var >-> arith.
Declare Scope arith_scope.
Infix "+" := Plus : arith_scope. Infix "+" := Plus : arith_scope.
Infix "-" := Minus : arith_scope. Infix "-" := Minus : arith_scope.
Infix "*" := Times : arith_scope. Infix "*" := Times : arith_scope.