Daily Archives: 2011/02/10

Beginning Ltac

One of the strong points of Coq is its powerful proof automation facility embodied in the tactic language . Instead of having to write new tactics in ML, compiling them, and jumping through all sorts of hoops in the process, … Continue reading

Posted in Coq | Tagged | Leave a comment