Tactics in the macro expander
Racket
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
ctt
engine Use local-expand-expression to prevent quadratic overhead Aug 31, 2017
hol Use goals on the proof-state consistently Feb 27, 2017
.gitignore Add HOL stuff Feb 24, 2017
README.md Add README Oct 26, 2016
expansion-handler.rkt Start of DrRacket tool Dec 9, 2016
goal.rkt Progress Mar 28, 2017
info.rkt Start of DrRacket tool Dec 9, 2016
lcf-example.rkt Begin refactor Feb 24, 2017
lcfish.rkt Use local-expand-expression to prevent quadratic overhead Aug 31, 2017
lift-errors.rkt Report multiple proof mistakes + more precise tooltips Dec 9, 2016
lift-holes.rkt Begin refactor Feb 24, 2017
lift-tooltips.rkt
new-tactics.rkt
rewindable-streams.rkt Implement thenl with rewindable streams Jun 7, 2017
rule.rkt Backport sealing improvements from the-machine Jun 22, 2017
seal.rkt Use local-expand-expression to prevent quadratic overhead Aug 31, 2017
stlc-lcfish.rkt Try to avoid some syntax/parse error message generation. Sep 12, 2017
stx-utils.rkt
syntax-info.rkt Start of DrRacket tool Dec 9, 2016
todo.rkt Clicking around does the right thing in the goal list Dec 12, 2016
tool.rkt Better display of current goal Dec 12, 2016
tooltip-info.rkt Better tooltip performance Apr 3, 2017

README.md

Macro tactics

Here are some experimental implementations of tactics in the macro expander.