equal
deleted
inserted
replaced
44 \ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
44 \ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
45 le{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ {\isasymequiv}\isanewline |
45 le{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ {\isasymequiv}\isanewline |
46 \ \ \ \ \ \ \ \ \ \ \ \ \ \ size\ xs\ {\isacharequal}\ size\ ys\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharless}size\ xs{\isachardot}\ xs{\isacharbang}i\ {\isacharless}{\isacharless}{\isacharequal}\ ys{\isacharbang}i{\isacharparenright}{\isachardoublequoteclose}% |
46 \ \ \ \ \ \ \ \ \ \ \ \ \ \ size\ xs\ {\isacharequal}\ size\ ys\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharless}size\ xs{\isachardot}\ xs{\isacharbang}i\ {\isacharless}{\isacharless}{\isacharequal}\ ys{\isacharbang}i{\isacharparenright}{\isachardoublequoteclose}% |
47 \begin{isamarkuptext}% |
47 \begin{isamarkuptext}% |
48 \noindent |
48 \noindent |
49 The infix function \isa{{\isacharbang}} yields the nth element of a list. |
49 The infix function \isa{{\isacharbang}} yields the nth element of a list, starting with 0. |
50 |
50 |
51 \begin{warn} |
51 \begin{warn} |
52 A type constructor can be instantiated in only one way to |
52 A type constructor can be instantiated in only one way to |
53 a given type class. For example, our two instantiations of \isa{list} must |
53 a given type class. For example, our two instantiations of \isa{list} must |
54 reside in separate theories with disjoint scopes. |
54 reside in separate theories with disjoint scopes. |