4 ms·
Oh wow! The paper [1] already introduces "tacticals", being functions from tactics to tactics that give you a very powerful language for composing tactics, and
by momentoftop 6y ago
Oh wow! The paper [1] already introduces "tacticals", being functions from tactics to tactics that give you a very powerful language for composing tactics, and its examples are still very close to what you would see in things like HOL Light:
(REPEAT GENTAC) THEN REPEAT (ANYCASESTAC THEN SIMPTAC).
Every one of these identifiers is an ordinary ML function. "THEN" is infix.
REPEAT : tactic -> tactic
GENTAC : tactic
ANYCASESTAC : tactic
THEN : tactic -> tactic -> tactic
SIMPTAC : tactic
[1] http://www-public.imtbs-tsp.eu/~gibson/Teaching/CSC4504/ReadingMaterial/GordonMMNW78.pdf http://www-public.imtbs-tsp.eu/~gibson/Teaching/CSC4504/Read...