Re: [Hol-info] Getting the original type of a constant

[Michael N. <Mic...@ni...>]

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 <ben...@gm...> 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
> hol...@li...
> 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.