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

Robert White ai.robert.wangshuai at gmail.com
Fri Jun 5 13:30:53 UTC 2015


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 <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
[Moving to ILLC of UvA from this Sep. ]
[New email address will be shuai.wang at student.uva.nl]
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150605/0e96c7bb/attachment.html>


More information about the opentheory-users mailing list