From 56af55f38a673ef0398d6062f2833f98ee2eab16 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 9 Feb 2020 14:50:46 -0500 Subject: [PATCH] Revising Interpreters before class --- Interpreters_template.v | 1 + 1 file changed, 1 insertion(+) diff --git a/Interpreters_template.v b/Interpreters_template.v index 5ed4380..d289bf9 100644 --- a/Interpreters_template.v +++ b/Interpreters_template.v @@ -249,6 +249,7 @@ Example factorial_ugly := * them from our examples. *) Coercion Const : nat >-> arith. Coercion Var : var >-> arith. +Declare Scope arith_scope. Infix "+" := Plus : arith_scope. Infix "-" := Minus : arith_scope. Infix "*" := Times : arith_scope.