This is the HOL4 answer to the question.
If you know the name and theory of the constant, then
prim_mk_const {Thy = thy, Name = name}
will give you back the constant “as defined”. So that
type_of (prim_mk_const {Thy = "min", Name = "="})
gives back
val it = ``:α -> α -> bool``: hol_type
To get the name and theory of a constant, you can call
dest_thy_const : term -> {Thy:string,Name:string,Ty:hol_type}
I hope this helps,
Michael
On 25 Sep 2014, at 6:40 am, Benja Fallenstein <[email protected]>
wrote:
> Hi all,
>
> I'm wondering whether there is a way to get the original type of a
> polymorphic constant -- e.g., given
>
> c = ``$= : num -> num -> bool``
>
> is there a way to obtain the most general type ``:'a -> 'a -> bool`` of the
> constant ``$=``?
>
> Thanks!
> - Benja
> ------------------------------------------------------------------------------
> Meet PCI DSS 3.0 Compliance Requirements with EventLog Analyzer
> Achieve PCI DSS 3.0 Compliant Status with Out-of-the-box PCI DSS Reports
> Are you Audit-Ready for PCI DSS 3.0 Compliance? Download White paper
> Comply to PCI DSS 3.0 Requirement 10 and 11.5 with EventLog Analyzer
> http://pubads.g.doubleclick.net/gampad/clk?id=154622311&iu=/4140/ostg.clktrk_______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
________________________________
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
------------------------------------------------------------------------------
Meet PCI DSS 3.0 Compliance Requirements with EventLog Analyzer
Achieve PCI DSS 3.0 Compliant Status with Out-of-the-box PCI DSS Reports
Are you Audit-Ready for PCI DSS 3.0 Compliance? Download White paper
Comply to PCI DSS 3.0 Requirement 10 and 11.5 with EventLog Analyzer
http://pubads.g.doubleclick.net/gampad/clk?id=154622311&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
