On 10/29/2012 11:34 PM, Michael Norrish wrote: > On 30/10/12 13:18, Tony Johnson wrote: > >>> It’s simple: the prove function doesn’t perform the tactic-validity >>> test. > > [..] > >> Has an error ever shown up because of this validity test not being >> checked in >> every case the tactic is ran? > > I can’t think of an instance, no. But, what do you mean by “error”? > > The basic LCF design means that soundness errors cannot occur because > of this check being omitted. In particular, tactic-validity has > nothing to do with the soundness of the kernel’s inferences. > > Michael >
Ok, so if I understand this correctly the validity checks are only in place to keep you from going down an inference chain that is guarenteed to go no where in making progress towards proving your goal. This being only an issue when searching for the proof itself in the interactive prompt, not when just verifying it. -Tony ------------------------------------------------------------------------------ Everyone hates slow websites. So do we. Make your web apps faster with AppDynamics Download AppDynamics Lite for free today: http://p.sf.net/sfu/appdyn_sfd2d_oct _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
