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

Comment AbstractInterpretation

Browse source
This commit is contained in:
Adam Chlipala 2016-03-06 20:30:05 -05:00
parent 0b204ccdad
commit 70974db013
4 changed files with 1969 additions and 1721 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3687
AbstractInterpretation.v
View file

File diff suppressed because it is too large Load diff

1
Frap.v
View file

@ -111,6 +111,7 @@ Ltac cases E :=
Global Opaque max min. Global Opaque max min.
Infix "==n" := eq_nat_dec (no associativity, at level 50). Infix "==n" := eq_nat_dec (no associativity, at level 50).
Infix "<=?" := le_lt_dec.
Export Frap.Map. Export Frap.Map.

1
README.md
View file

@ -11,3 +11,4 @@ Just run `make` here to build everything, including the book `frap.pdf` and the
* Chapter 4: `TransitionSystems.v` * Chapter 4: `TransitionSystems.v`
* Chapter 5: `ModelChecking.v` * Chapter 5: `ModelChecking.v`
* Chapter 6: `OperationalSemantics.v` * Chapter 6: `OperationalSemantics.v`
* Chapter 7: `AbstractInterpretation.v`

1
_CoqProject
View file

@ -17,3 +17,4 @@ ModelChecking_template.v
ModelChecking.v ModelChecking.v
OperationalSemantics_template.v OperationalSemantics_template.v
OperationalSemantics.v OperationalSemantics.v
AbstractInterpretation.v