Perhaps use ty_antiq ? So: > - val tp1 = ==`:'a`==; >> val tp1 = ``:'a`` : hol_type
> - val p1 = (--`p1:tp1`--); > ! Uncaught exception: -- Hmm, I thought that tp1 was a type Instead do: val p1 = --`p1:^(ty_antiq tp1)`-- ; > - val tp2 = ==`:(tp1)list`==; > ! Uncaught exception: And here you just forget to antiquote tp1; so: vap tp2 = ==`:(^tp1)list`==; --Wish. ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
