I hope folks can help me improve my code readable.ml, which in the new
subversion 166 is in
hol_light/RichterHilbertAxiomGeometry/
1) Can you pretty-print error messages in HOL Light? E.g. here:
with Not_found -> failwith("missing initial \"proof\" or final \"qed;\" in "^ s)
It would be nice
Hi Bill,
Le 2013-07-02 à 00:00, Bill Richter a écrit :
> I hope folks can help me improve my code readable.ml, which in the new
> subversion 166 is in
> hol_light/RichterHilbertAxiomGeometry/
>
> 1) Can you pretty-print error messages in HOL Light? E.g. here:
>
> with Not_found -> failwith