Matthew Brecknell mbrcknl
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {- | |
| An unholy mix of | |
| • Conor McBride, “Dependently typed metaprogramming” | |
| http://www.cl.cam.ac.uk/~ok259/agda-course-13/ | |
| • Oleg Kiselyov, “Typed tagless final interpreters” | |
| http://okmij.org/ftp/tagless-final/course/ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| synonyms: | |
| >> | |
| \\ | |
| THEN | |
| ( means ";" in Isar ) | |
| meaning: | |
| tac1 \\ tac2 | |
| means apply tac1 to the current proof state | |
| then apply tac2 to all the resulting subgoals |