On 01/04/2013 10:40, Petros Papapanagiotou wrote:
>
> You may also want to catch any exceptions and give more meaningful error
> messages, but it is up to you how you want to handle failures.
>
Actually I just noticed John has updated the error messages of
X_CHOOSE_TAC recently (in the spirit of Vincent's approach to providing
better type checking feedback I am guessing). I should propagate these
changes!
Also note that the "is_vartype" check in my code is actually restricting
and can be omitted. Here is a new more generalised version:
let try_type tp tm =
try inst (type_match (type_of tm) tp []) tm
with Failure _ -> tm;;
let (disj_term: term -> term -> term) =
fun t1 t2 -> mk_disj (try_type `:bool` t1, try_type `:bool` t2);;
Regards,
Petros
--
Petros Papapanagiotou
CISA, School of Informatics
The University of Edinburgh
Email: p.papapanagio...@sms.ed.ac.uk
---
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
------------------------------------------------------------------------------
Own the Future-Intel® Level Up Game Demo Contest 2013
Rise to greatness in Intel's independent game demo contest.
Compete for recognition, cash, and the chance to get your game
on Steam. $5K grand prize plus 10 genre and skill prizes.
Submit your demo by 6/6/13. http://p.sf.net/sfu/intel_levelupd2d
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
