Re: [isabelle] debugging Isar



On Thu, 28 Feb 2008, Jeremy Dawson wrote:

> Thanks for your reply - as a matter of fact I did something like that, to the
> point where I found the problem is in len_ty_tac.  But len_ty_tac isn't
> composed of smaller tactics, rather it looks at the subgoal and goes from
> there, thus
> 
> fun len_ty_tac sg st =
>  let val cg = List.nth (cprems_of st, sg - 1) ;
>    val len_st = thin_len RSN (sg, st) ;
>    val len_cp = List.nth (cprems_of len_st, sg - 1) ;

For debugging you may use ML {* Isar.state () *} or ML {* Isar.goal () *} 
to get full access to whatever state the toplevel is presently in.

Also note that the above List.nth method to access a particular subgoal is 
a bit fragile, it just breaks if "sg" is out of range, while the usual 
convention is to make the tactic fail with an empty result sequence.  The 
existing tacticals SUBGOAL and the newer CSUBGOAL will do the job for you.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.