Adam Chlipala
7bc0425ccf
Merge pull request #39 from bkushigian/patch-1
...
Fixed markdown inline
2020-03-29 10:20:51 -04:00
Ben A Kushigian
01ad154c5a
Fixed markdown inline
...
was
```
`make lib'
```
should be
```
`make lib`
```
2020-03-28 15:07:21 -07:00
Adam Chlipala
b5e1ae0c29
Clarify what linear_arithmetic does these days
2020-03-17 15:50:19 -04:00
Adam Chlipala
72c0bc3a04
Merge pull request #38 from mdempsky/parity-subtract
...
Add missing "O - O = E" abstraction case
2020-03-17 11:24:57 -04:00
Adam Chlipala
c502399de4
Separate out library code with its own license
2020-03-17 09:22:06 -04:00
Matthew Dempsky
ebcd23ee6c
Add missing "O - O = E" abstraction case
...
This case is implemented by parity_subtract in
AbstractInterpretation.v and is necessary to calculate the "most
precise abstraction."
See also #28 , #37 .
2020-03-16 12:58:20 -07:00
Adam Chlipala
51a7fae33e
Unnecessary Fixpoint
2020-03-11 09:40:55 -04:00
Adam Chlipala
dd266f2d8c
Proofreading and Coq-version-updating AbstractInterpretation
2020-03-07 15:32:50 -05:00
Adam Chlipala
64fe989cdb
Turn off some warnings
2020-03-04 11:51:34 -05:00
Adam Chlipala
19d915fb37
Merge pull request #36 from samuelgruetter/ltac_lecture_comment
...
explain why recursive [inster] can fail
2020-03-02 11:45:36 -05:00
Samuel Gruetter
74e2399343
explain why recursive [inster] can fail
2020-03-01 22:30:35 -05:00
Adam Chlipala
096b69a3e9
Update LogicProgramming for Coq 8.10
2020-03-01 10:39:01 -05:00
Adam Chlipala
d6e8cebdc9
Revising OperationalSemantics
2020-02-29 16:10:37 -05:00
Adam Chlipala
254e2aedc6
Tiny copy-editing
2020-02-23 16:20:39 -05:00
Adam Chlipala
c2f56e1b5f
Merge branch 'master' of github.com:achlipala/frap
2020-02-23 14:58:58 -05:00
Adam Chlipala
49af9ea6a9
Merge pull request #34 from samuelgruetter/ltac_lecture
...
preparing Ltac lecture
2020-02-23 14:58:38 -05:00
Samuel Gruetter
d49ca3afa8
typo
2020-02-19 17:27:11 -05:00
Samuel Gruetter
f5ca4613d7
preparing Ltac lecture
2020-02-17 23:55:43 -05:00
Adam Chlipala
aace3dfb02
Changes based on feedback from Christopher McNally (mcncm, in #33 )
2020-02-16 11:09:31 -05:00
Adam Chlipala
728a8255f8
A little more text for the new FirstClassFunctions examples
2020-02-15 12:32:36 -05:00
Adam Chlipala
af19eb9f42
Update FirstClassFunctions_template from new source material
2020-02-12 14:03:15 -05:00
Adam Chlipala
6f17daa2df
FirstClassFunctions compiles again
2020-02-12 13:53:55 -05:00
Adam Chlipala
fbf211bad2
Merge branch 'master' of github.com:achlipala/frap
2020-02-12 08:01:22 -05:00
Adam Chlipala
6ea006fccf
Truly building with Coq 8.9 again
2020-02-10 13:53:26 -05:00
Adam Chlipala
77f22213d8
Avoid a command only introduced in Coq 8.10, so that 8.9 keeps working
2020-02-10 13:44:35 -05:00
Adam Chlipala
c863b12c5b
FirstClassFunctions: combinators for tree traversals, applied to the Interpreters imperative language
2020-02-09 16:44:22 -05:00
Adam Chlipala
fb3c957cd8
FirstClassFunctions: facts about how operations don't grow sizes
2020-02-09 15:56:25 -05:00
Adam Chlipala
0eea46080f
FirstClassFunctions: start of a new example with a language of functions over dynamically typed values
2020-02-09 14:52:00 -05:00
Adam Chlipala
56af55f38a
Revising Interpreters before class
2020-02-09 14:50:46 -05:00
Adam Chlipala
c050ec21ae
Proofreading FirstClassFunctions
2020-02-09 13:17:48 -05:00
Adam Chlipala
a0993b537d
Revising Interpreters before class
2020-02-09 12:54:33 -05:00
Adam Chlipala
5e0e034263
Bump required Coq version
2020-02-09 12:26:32 -05:00
Adam Chlipala
f049d7e824
Scope fix for new N support
2020-02-08 15:18:00 -05:00
Adam Chlipala
c611524a96
Prevent more warnings for Coq 8.10
2020-02-08 15:15:38 -05:00
Adam Chlipala
0ed668481d
Some N-related library content contributed by Sam Gruetter
2020-02-08 14:56:10 -05:00
Adam Chlipala
89863fd999
Make 'cases' tactic handle disjunction
2020-02-08 14:47:19 -05:00
Adam Chlipala
5a28d4fe6a
Replace omega with lia
2020-02-08 14:41:07 -05:00
Adam Chlipala
d41373e0cb
Link to Spring 2020 users of the book
2020-02-08 10:46:47 -05:00
Adam Chlipala
295e095e98
Polymorphism: 8.10 update
2020-02-04 17:46:37 -05:00
Adam Chlipala
152b90e9ef
Merge
2020-02-02 17:19:40 -05:00
Adam Chlipala
89f21b8533
First phase of update for Coq 8.10
2020-02-02 17:16:19 -05:00
Adam Chlipala
958906a2e5
Clarify Cartesian-product operator
2020-01-08 14:36:27 -05:00
Adam Chlipala
93ef5add7a
Closes #28
2019-03-04 11:28:37 -05:00
Adam Chlipala
ed64e05e38
Closes #27
2019-03-04 11:26:06 -05:00
Adam Chlipala
e032ab4240
Update for Coq 8.9
2019-03-04 11:23:01 -05:00
Adam Chlipala
e92a697e33
Link to CSE 505 at UW
2018-10-27 08:22:04 -04:00
Adam Chlipala
79e5f916b5
Merge pull request #26 from bmsherman/book_typo
...
Fix typo in book with label for Embeddings chapter
2018-05-29 14:45:32 -04:00
Ben Sherman
6e1e2b7ab1
Fix typo in book with label for Embeddings chapter
2018-05-25 10:44:08 -04:00
Adam Chlipala
970580d6f9
SessionTypes: LaTeX finished
2018-05-15 15:27:57 -04:00
Adam Chlipala
7ca4318d66
SessionTypes: almost done with LaTeX chapter
2018-05-14 18:09:22 -04:00