equal
deleted
inserted
replaced
497 } |
497 } |
498 \isamarkuptrue% |
498 \isamarkuptrue% |
499 % |
499 % |
500 \begin{isamarkuptext}% |
500 \begin{isamarkuptext}% |
501 For convenience, the default \isa{HOL} setup for \isa{Haskell} |
501 For convenience, the default \isa{HOL} setup for \isa{Haskell} |
502 maps the \isa{eq} class to its counterpart in \isa{Haskell}, |
502 maps the \isa{equal} class to its counterpart in \isa{Haskell}, |
503 giving custom serialisations for the class \isa{eq} (by command |
503 giving custom serialisations for the class \isa{equal} (by command |
504 \indexdef{}{command}{code\_class}\hypertarget{command.code-class}{\hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}}) and its operation \isa{eq{\isacharunderscore}class{\isachardot}eq}% |
504 \indexdef{}{command}{code\_class}\hypertarget{command.code-class}{\hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}}) and its operation \isa{equal{\isacharunderscore}class{\isachardot}equal}% |
505 \end{isamarkuptext}% |
505 \end{isamarkuptext}% |
506 \isamarkuptrue% |
506 \isamarkuptrue% |
507 % |
507 % |
508 \isadelimquotett |
508 \isadelimquotett |
509 % |
509 % |
510 \endisadelimquotett |
510 \endisadelimquotett |
511 % |
511 % |
512 \isatagquotett |
512 \isatagquotett |
513 \isacommand{code{\isacharunderscore}class}\isamarkupfalse% |
513 \isacommand{code{\isacharunderscore}class}\isamarkupfalse% |
514 \ eq\isanewline |
514 \ equal\isanewline |
515 \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}{\isacharparenright}\isanewline |
515 \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}{\isacharparenright}\isanewline |
516 \isanewline |
516 \isanewline |
517 \isacommand{code{\isacharunderscore}const}\isamarkupfalse% |
517 \isacommand{code{\isacharunderscore}const}\isamarkupfalse% |
518 \ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline |
518 \ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline |
519 \ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}% |
519 \ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}% |
524 % |
524 % |
525 \endisadelimquotett |
525 \endisadelimquotett |
526 % |
526 % |
527 \begin{isamarkuptext}% |
527 \begin{isamarkuptext}% |
528 \noindent A problem now occurs whenever a type which is an instance |
528 \noindent A problem now occurs whenever a type which is an instance |
529 of \isa{eq} in \isa{HOL} is mapped on a \isa{Haskell}-built-in type which is also an instance of \isa{Haskell} |
529 of \isa{equal} in \isa{HOL} is mapped on a \isa{Haskell}-built-in type which is also an instance of \isa{Haskell} |
530 \isa{Eq}:% |
530 \isa{Eq}:% |
531 \end{isamarkuptext}% |
531 \end{isamarkuptext}% |
532 \isamarkuptrue% |
532 \isamarkuptrue% |
533 % |
533 % |
534 \isadelimquote |
534 \isadelimquote |
538 \isatagquote |
538 \isatagquote |
539 \isacommand{typedecl}\isamarkupfalse% |
539 \isacommand{typedecl}\isamarkupfalse% |
540 \ bar\isanewline |
540 \ bar\isanewline |
541 \isanewline |
541 \isanewline |
542 \isacommand{instantiation}\isamarkupfalse% |
542 \isacommand{instantiation}\isamarkupfalse% |
543 \ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline |
543 \ bar\ {\isacharcolon}{\isacharcolon}\ equal\isanewline |
544 \isakeyword{begin}\isanewline |
544 \isakeyword{begin}\isanewline |
545 \isanewline |
545 \isanewline |
546 \isacommand{definition}\isamarkupfalse% |
546 \isacommand{definition}\isamarkupfalse% |
547 \ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline |
547 \ {\isachardoublequoteopen}HOL{\isachardot}equal\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline |
548 \isanewline |
548 \isanewline |
549 \isacommand{instance}\isamarkupfalse% |
549 \isacommand{instance}\isamarkupfalse% |
550 \ \isacommand{by}\isamarkupfalse% |
550 \ \isacommand{by}\isamarkupfalse% |
551 \ default\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq{\isacharunderscore}bar{\isacharunderscore}def{\isacharparenright}\isanewline |
551 \ default\ {\isacharparenleft}simp\ add{\isacharcolon}\ equal{\isacharunderscore}bar{\isacharunderscore}def{\isacharparenright}\isanewline |
552 \isanewline |
552 \isanewline |
553 \isacommand{end}\isamarkupfalse% |
553 \isacommand{end}\isamarkupfalse% |
554 % |
554 % |
555 \endisatagquote |
555 \endisatagquote |
556 {\isafoldquote}% |
556 {\isafoldquote}% |
585 % |
585 % |
586 \endisadelimquotett |
586 \endisadelimquotett |
587 % |
587 % |
588 \isatagquotett |
588 \isatagquotett |
589 \isacommand{code{\isacharunderscore}instance}\isamarkupfalse% |
589 \isacommand{code{\isacharunderscore}instance}\isamarkupfalse% |
590 \ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline |
590 \ bar\ {\isacharcolon}{\isacharcolon}\ equal\isanewline |
591 \ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}% |
591 \ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}% |
592 \endisatagquotett |
592 \endisatagquotett |
593 {\isafoldquotett}% |
593 {\isafoldquotett}% |
594 % |
594 % |
595 \isadelimquotett |
595 \isadelimquotett |