pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-09-19 11:47:12 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
583 commits 1 branch 0 tags 1.6 MiB
Commit graph

583 commits

This branch
This branch
All branches
Author SHA1 Message Date
Adam Chlipala
55d128d988 Italicize a term on first use (thanks to Todd Morley for the suggestion) 2024-06-06 07:52:32 -04:00
Adam Chlipala
d9fb7fca94 Wrong tactic name in comment 2023-04-23 16:09:47 -04:00
Adam Chlipala
ac0a15e9f2 Rename typing relations from hasty to has_ty 2023-03-19 11:59:34 -04:00
Adam Chlipala
04be648f88 Note required Coq version 2023-02-19 16:23:56 -05:00
Adam Chlipala
2ef93d36fc Typo fix 2023-02-19 13:42:53 -05:00
Adam Chlipala
172716c8ef Latest MIT offering finished 2022-08-21 08:59:23 -04:00
Adam Chlipala
28ff5cb550 Revising for Wednesday's lecture 2022-04-18 12:58:53 -04:00
Adam Chlipala
092e3ccc1b Revising for next Wednesday's lecture 2022-04-03 14:40:20 -04:00
Adam Chlipala
0e13a0a695 Revising for tomorrow's lecture 2022-04-03 14:02:22 -04:00
Adam Chlipala
33733a0450 Revising for this week's lectures 2022-03-27 13:40:08 -04:00
Adam Chlipala
c5a69b6253 Revising for tomorrow's lecture 2022-03-13 18:10:19 -04:00
Adam Chlipala
f3211734b9 A big pass to stop Coq from complaining about missing locality annotations 2022-03-07 13:48:40 -05:00
Adam Chlipala
b643755628
Merge pull request #57 from al3623/master 
Change precedence of map includes operator according to spring 21 TODO
 2022-03-07 09:05:46 -05:00
Amanda Liu
b2eafc94bf Change precedence of map includes operator according to spring 21 TODO 2022-03-06 23:01:31 -05:00
Adam Chlipala
955fd59327 Revising for Wednesday's lecture 2022-03-06 14:47:05 -05:00
Adam Chlipala
eb53c0d714 Revising for tomorrow's lecture 2022-03-06 14:10:06 -05:00
Adam Chlipala
52e47df705 Revising for Monday's lecture 2022-02-26 15:58:03 -05:00
Adam Chlipala
e3f0ada30e Revising for Wednesday's lecture 2022-02-20 12:29:17 -05:00
Adam Chlipala
ddacd030e6 Revising for Tuesday's lecture 2022-02-20 12:02:38 -05:00
Adam Chlipala
23a0972d11 Revising for Wednesday's lecture 2022-02-13 14:34:23 -05:00
Adam Chlipala
0cba7c9f61 Revising for tomorrow's lecture 2022-02-13 14:16:33 -05:00
Adam Chlipala
22118d90be Update AbstractInterpretation for newer Coq versions 2022-02-06 13:13:29 -05:00
Adam Chlipala
c2260bb22b
Merge pull request #56 from al3623/cases_on_N 
Update cases tactic to work on N type
 2022-02-06 13:04:19 -05:00
Adam Chlipala
65b817d7ae Revising for Wednesday's lecture 2022-02-06 13:03:43 -05:00
Amanda Liu
1bff5420e2 Update cases tactic to work on N type 2022-02-06 12:47:50 -05:00
Adam Chlipala
bec1b1b919 Revising for tomorrow's lecture 2022-02-06 12:35:54 -05:00
Adam Chlipala
f428750fdf Change notation to remain compatible with multiple Coq versions 2022-01-31 21:02:31 -05:00
Adam Chlipala
0f72c50df0 Revising for next next lecture 2022-01-29 17:22:33 -05:00
Adam Chlipala
6c1d09bbbc Revising for next lecture 2022-01-29 16:28:31 -05:00
Adam Chlipala
d745f0802e Ported to Coq 8.15 2022-01-29 15:13:09 -05:00
Adam Chlipala
1b43aa9aea Typo in function definition 2021-07-02 12:58:22 -04:00
Adam Chlipala
3582bd1222 Typo in operational semantics 2021-05-30 16:09:34 -04:00
Adam Chlipala
6986124c34 Update code index with this semester's chapter additions 2021-05-19 17:01:51 -04:00
Adam Chlipala
35d15a765d Revising for the final week of class 2021-05-16 11:55:01 -04:00
Adam Chlipala
8fdc4e2cfd Revising before this week's lectures 2021-05-10 10:45:34 -04:00
Adam Chlipala
45fa64d69e Revising for this week's lectures 2021-05-02 12:56:47 -04:00
Adam Chlipala
7e4068d5db Revising for Wednesday's lecture 2021-04-24 15:55:15 -04:00
Adam Chlipala
513e01bd3b Revising before next lecture 2021-04-24 12:59:10 -04:00
Adam Chlipala
b549b15af7 Revising for next lecture 2021-04-18 16:23:25 -04:00
Adam Chlipala
796fc8d64c Noticed one invariant in HoareLogic was more complex than required 2021-04-12 16:03:38 -04:00
Adam Chlipala
1d93f6f994
Merge pull request #55 from cpitclaudel/hoare_tweaks 
Two tweaks in HoareLogic.v
 2021-04-12 16:01:44 -04:00
Clément Pit-Claudel
1e81721268 Make the ht1 tactic a bit more robust in HoareLogic.v 
(Without this change, the HtIf rule can fail to generalize and unify spuriously
with goals of the right shape)
 2021-04-12 15:07:34 -04:00
Clément Pit-Claudel
2ed1d52171 Get rid of the “reset” scope in HoareLogic.v 
It's not needed, and it makes everything harder to read.
 2021-04-12 15:04:56 -04:00
Adam Chlipala
899b3dee24 Revising for this week's lectures 2021-04-11 13:32:38 -04:00
Adam Chlipala
45124f3686 Revising for Wednesday's lecture 2021-04-04 14:51:02 -04:00
Adam Chlipala
d177e9fb6f Revising for tomorrow's lecture 2021-04-04 14:28:23 -04:00
Adam Chlipala
1664ddb531 EvaluationContexts_template 2021-03-30 16:12:37 -04:00
Adam Chlipala
ffde22e9c9 Typo fix 2021-03-29 09:35:17 -04:00
Adam Chlipala
1c69525dc5 Typo fix 2021-03-29 09:28:33 -04:00
Adam Chlipala
75ea3ed0b3 Chapter renumbering 2021-03-28 17:03:56 -04:00