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

Unnecessary Fixpoint

Browse source
This commit is contained in:
Adam Chlipala 2020-03-11 09:40:55 -04:00
parent dd266f2d8c
commit 51a7fae33e
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
CompilerCorrectness.v
View file

@ -901,7 +901,7 @@ Compute tempVar 2.
* lack of clashes. We also prove some properties that will come in handy * lack of clashes. We also prove some properties that will come in handy
* later. *) * later. *)
Fixpoint noUnderscoreVar (x : var) : bool := Definition noUnderscoreVar (x : var) : bool :=
match x with match x with
| String "_" _ => false | String "_" _ => false
| _ => true | _ => true

2
CompilerCorrectness_template.v
View file

@ -613,7 +613,7 @@ Compute tempVar 0.
Compute tempVar 1. Compute tempVar 1.
Compute tempVar 2. Compute tempVar 2.
Fixpoint noUnderscoreVar (x : var) : bool := Definition noUnderscoreVar (x : var) : bool :=
match x with match x with
| String "_" _ => false | String "_" _ => false
| _ => true | _ => true