3 ms·
Edinburgh LCF already had tactics, both the book about it and the paper "A Metalanguage for Interactive Proof in LCF" from 1978 mention it and I wouldn't be sur
by ImprobableTruth 6y ago
Edinburgh LCF already had tactics, both the book about it and the paper "A Metalanguage for Interactive Proof in LCF" from 1978 mention it and I wouldn't be surprised if there was an even earlier mention. Pretty crazy to think about how ML was devised to allow a safe working with tactics.
- momentoftop 6y agoOh 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...