I just noticed that Voevodsky's Homotopy Type Theory book deals on p 7 with
issues I've posted here:
http://hottheory.files.wordpress.com/2013/03/hott-online.pdf
One difficulty often encountered by the classical mathematician when
faced with learning about type theory is that [it is not eve
Ta.
On Mon, Jun 24, 2013 at 4:27 PM, Konrad Slind wrote:
> Globals.max_print_depth
>
>
> On Mon, Jun 24, 2013 at 10:03 AM, Ramana Kumar
> wrote:
>
>> Is there a notion of print depth for the HOL printer, to avoid printing
>> very large terms in full? (Using PolyML.print_depth doesn't seem to do
Globals.max_print_depth
On Mon, Jun 24, 2013 at 10:03 AM, Ramana Kumar wrote:
> Is there a notion of print depth for the HOL printer, to avoid printing
> very large terms in full? (Using PolyML.print_depth doesn't seem to do the
> right thing.)
>
>
> -
Is there a notion of print depth for the HOL printer, to avoid printing
very large terms in full? (Using PolyML.print_depth doesn't seem to do the
right thing.)
--
This SF.net email is sponsored by Windows:
Build for Windo
