Closed ccodel closed 6 months ago
A bunch of lemmas were added to Model/Subst.lean, and the example file from the Formal Cookies talk was added to the Examples/ folder.
Model/Subst.lean
Examples/
Notes: compare substL (line 151) to subst (line 185), and see the TODO on line 219.
substL
subst
Better notation/syntax? See lines 49-53.
A bunch of lemmas were added to
Model/Subst.lean, and the example file from the Formal Cookies talk was added to theExamples/folder.Notes: compare
substL(line 151) tosubst(line 185), and see the TODO on line 219.Better notation/syntax? See lines 49-53.