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

CompilerCorrectness_template

Browse source
This commit is contained in:
Adam Chlipala 2017-03-19 20:09:48 -04:00
parent 5df1caf940
commit 88df5601f5
3 changed files with 1381 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
CompilerCorrectness.v
View file

@ -178,8 +178,8 @@ Example month_boundaries_in_days :=
* because the program does not terminate, generating new output infinitely * because the program does not terminate, generating new output infinitely
* often. *) * often. *)
Hint Extern 1 (interp _ _ = _) => simplify; congruence. Hint Extern 1 (interp _ _ = _) => simplify; equality.
Hint Extern 1 (interp _ _ <> _) => simplify; congruence. Hint Extern 1 (interp _ _ <> _) => simplify; equality.
Theorem first_few_values : Theorem first_few_values :
generate ($0, month_boundaries_in_days) [Some 28; Some 56]. generate ($0, month_boundaries_in_days) [Some 28; Some 56].

1378
CompilerCorrectness_template.v Normal file
View file

File diff suppressed because it is too large Load diff

1
_CoqProject
View file

@ -30,6 +30,7 @@ LogicProgramming.v
LogicProgramming_template.v LogicProgramming_template.v
AbstractInterpretation.v AbstractInterpretation.v
CompilerCorrectness.v CompilerCorrectness.v
CompilerCorrectness_template.v
LambdaCalculusAndTypeSoundness_template.v LambdaCalculusAndTypeSoundness_template.v
LambdaCalculusAndTypeSoundness.v LambdaCalculusAndTypeSoundness.v
TypesAndMutation.v TypesAndMutation.v