Commit graph

14 commits

Author SHA1 Message Date
Adam Chlipala
d745f0802e Ported to Coq 8.15 2022-01-29 15:13:09 -05:00
Adam Chlipala
8fdc4e2cfd Revising before this week's lectures 2021-05-10 10:45:34 -04:00
Adam Chlipala
75ea3ed0b3 Chapter renumbering 2021-03-28 17:03:56 -04:00
Adam Chlipala
d3c7a85b49 More cleanup around addition of RuleInduction 2021-03-01 12:15:34 -05:00
Adam Chlipala
300f78191e Revising before class 2020-04-26 14:30:18 -04:00
Adam Chlipala
213f8b270b Revising before class 2020-04-26 14:28:52 -04:00
Adam Chlipala
7e84adc6bd ProgramDerivation_template 2018-05-06 19:49:10 -04:00
Adam Chlipala
a8239e7925 Commented ProgramDerivation, with chapter renumbering in Coq code 2018-05-06 12:53:49 -04:00
Adam Chlipala
5f981335d9 ProgramDerivation: adding caches 2018-05-05 18:51:21 -04:00
Adam Chlipala
3ff400b780 ProgramDerivation: derivation of split counter 2018-05-05 15:19:12 -04:00
Adam Chlipala
4505284871 ProgramDerivation: refine_method and refine_rep 2018-05-05 14:40:51 -04:00
Adam Chlipala
2f5635938c ProgramDerivation: ADT refinement reflexivity and transitivity 2018-05-05 14:11:37 -04:00
Adam Chlipala
4171f5c286 ProgramDerivation: ADT refinement and one general principle for it 2018-05-05 12:51:46 -04:00
Adam Chlipala
cf67854a42 ProgramDerivation: starting with example from Fiat tutorial 2018-05-05 10:35:53 -04:00