equal
deleted
inserted
replaced
889 \hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ |
889 \hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ |
890 \hspace*{0pt}\\ |
890 \hspace*{0pt}\\ |
891 \hspace*{0pt}fun null [] = true\\ |
891 \hspace*{0pt}fun null [] = true\\ |
892 \hspace*{0pt} ~| null (x ::~xs) = false;\\ |
892 \hspace*{0pt} ~| null (x ::~xs) = false;\\ |
893 \hspace*{0pt}\\ |
893 \hspace*{0pt}\\ |
894 \hspace*{0pt}fun eq{\char95}nat (Suc a) Zero{\char95}nat = false\\ |
894 \hspace*{0pt}fun eq{\char95}nat (Suc nat') Zero{\char95}nat = false\\ |
895 \hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat (Suc a) = false\\ |
895 \hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat (Suc nat') = false\\ |
896 \hspace*{0pt} ~| eq{\char95}nat (Suc nat) (Suc nat') = eq{\char95}nat nat nat'\\ |
896 \hspace*{0pt} ~| eq{\char95}nat (Suc nat) (Suc nat') = eq{\char95}nat nat nat'\\ |
897 \hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat Zero{\char95}nat = true;\\ |
897 \hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat Zero{\char95}nat = true;\\ |
898 \hspace*{0pt}\\ |
898 \hspace*{0pt}\\ |
899 \hspace*{0pt}datatype monotype = Mono of nat * monotype list;\\ |
899 \hspace*{0pt}datatype monotype = Mono of nat * monotype list;\\ |
900 \hspace*{0pt}\\ |
900 \hspace*{0pt}\\ |