pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-27 23:06:20 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Revising for next lecture

Browse source
This commit is contained in:
Adam Chlipala 2022-01-29 16:28:31 -05:00
parent d745f0802e
commit 6c1d09bbbc
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
BasicSyntax.v
View file

@ -206,7 +206,7 @@ Module ArithWithVariables.
* We use an infix operator [==v] for equality tests on strings. * We use an infix operator [==v] for equality tests on strings.
* It has a somewhat funny and very expressive type, * It has a somewhat funny and very expressive type,
* whose details we will try to gloss over. * whose details we will try to gloss over.
* (To dig into it more on your own, the appropriate keyword is "dependent types.") *) * (We later return to them in SubsetTypes.v.) *)
Fixpoint substitute (inThis : arith) (replaceThis : var) (withThis : arith) : arith := Fixpoint substitute (inThis : arith) (replaceThis : var) (withThis : arith) : arith :=
match inThis with match inThis with
| Const _ => inThis | Const _ => inThis
@ -469,7 +469,7 @@ Module ArithWithVariables.
linear_arithmetic. linear_arithmetic.
Qed. Qed.
Hint Rewrite n_times_0. Local Hint Rewrite n_times_0.
(* Registering rewrite hints will get [simplify] to apply them for us (* Registering rewrite hints will get [simplify] to apply them for us
* automatically! *) * automatically! *)