[opentheory-users] What is "asms" doing (from import)

[Joe Leslie-Hurd]

Hi Robert,

This beast is one of the OpenTheory axioms in its expanded form, as we
discussed recently:

http://www.gilith.com/opentheory/mailing-list/2015-June/000501.html

When you import a theory you are required to link the external symbols
(i.e., constants and type operators) to symbols in the logical
context, and also to satisfy the theory assumptions with theorems in
the logical context.

In normal situations no one would have to see this unparsable axiom,
because it is only used by the standard theory library, which contains
a set of theories already formalized in each theorem prover in the HOL
family, but the axiom is indeed present in the HOL Light logical
context and can be accessed as a theorem using the "axioms" function.

Cheers,

Joe

On Fri, Jun 5, 2015 at 6:30 AM, Robert White
<ai.robert.wangshuai at gmail.com> wrote:
> Dear Joe,
>
> I noticed that after reading it in, say the bool.art. We suppose to have a
> list of thm (of course) but I noticed there is also a list of assumptions.
> And the asms for bool.art is even not parsable:
>
>
>  ([([], `(\a. = a (\b. = (\c. c) (\c. c))) (\d. = (\e. d e) d)`);
>     ([],
>      `(\a. = a (\b. = (\c. c) (\c. c)))
>       (\d. (\e. = e (\f. = (\c. c) (\c. c)))
>            (\g. (\h i.
>                      =
>                      ((\j k.
>                            = (\l. l j k)
>                            (\m. m (= (\c. c) (\c. c)) (= (\c. c) (\c. c))))
>                       h
>                      i)
>                      h)
>                 (d g)
>                 (d (@ d))))`)],
>
>
> Now I am very confused what this "asms" is here for. I can't even
> (meaningfully) read the first line :(
>
> Thanks very much!
> --
>
> Regards,
> Robert White (Shuai Wang)
> INRIA Deducteam
> [Moving to ILLC of UvA from this Sep. ]
> [New email address will be shuai.wang at student.uva.nl]
>