Le 16.04.13 00:55, Bill Richter a écrit :
> Vince, thanks for fixing my error! This works now:
> let parse_qproof s = (fst o parse_preterm o lex o explode) (String.sub s 1
> (String.length s - 1));;
>
> Now I get the same output for both
> `;&1 + 1`;;
> and, with your new quotexpander,
> `'&1 + 1`;;
> val it : preterm =
> Combp
> (Combp (Varp ("+", Ptycon ("", [])),
> Combp (Varp ("&", Ptycon ("", [])), Varp ("1", Ptycon ("", [])))),
> Varp ("1", Ptycon ("", [])))
>
> That's great you're changing your Q-like module right now to use the parser
> instead of strings.
I'll do it if the new preterm parser gets integrated in HOL Light.
> Let me be more precise about environments, or as precise as I can be with my
> poor understanding of how words like scope and variable binding are used in
> HOL. Let's say in HOL Light that a free variable occurrence is in the scope
> of a variable binding. I think the variable is given the bound value, if we
> type it correctly, but its type is not inferred.
Could you give an example?
>
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://users.encs.concordia.ca/~vincent/
------------------------------------------------------------------------------
Precog is a next-generation analytics platform capable of advanced
analytics on semi-structured data. The platform includes APIs for building
apps and a phenomenal toolset for data science. Developers can use
our toolset for easy data analysis & visualization. Get a free account!
http://www2.precog.com/precogplatform/slashdotnewsletter
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
