+++ /dev/null
-
-
---================================================================================
-Simplified:
-`$d5' ::
- `{PrelBase.Eval (Pair a{-r3R-} b{-r3S-})}'
-`$d5' =
- _/\_ `a{-s1g3-}' `b{-s1g4-}' ->
- `PrelBase.void'
-`$d4' ::
- `{PrelBase.Eval (LList alpha{-r3P-})}'
-`$d4' =
- _/\_ `alpha{-s1g5-}' ->
- `PrelBase.void'
-`$d2' ::
- `{PrelBase.Eval (Tree x{-r3M-})}'
-`$d2' =
- _/\_ `x{-s1g6-}' ->
- `PrelBase.void'
-`$d1' ::
- `{PrelBase.Eval (A a{-r3K-})}'
-`$d1' =
- _/\_ `a{-s1g7-}' ->
- `PrelBase.void'
-`MkPair' ::
- `a{-r3R-} -> b{-r3S-} -> Pair a{-r3R-} b{-r3S-}'
-`MkPair' =
- _/\_ `a{-s1fQ-}' `b{-s1fR-}' -> \ `tpl' ::
- `a{-s1fQ-}'
- `tpl' `tpl' ::
- `b{-s1fR-}'
- `tpl' ->
- `MkPair'
- {_@_ `a{-s1fQ-}' _@_ `b{-s1fR-}' `tpl' `tpl'}
-`MkA' ::
- `a{-r3K-} -> A a{-r3K-} -> A a{-r3K-}'
-`MkA' =
- _/\_ `a{-s1fS-}' -> \ `tpl' ::
- `a{-s1fS-}'
- `tpl' `tpl' ::
- `A a{-s1fS-}'
- `tpl' ->
- `MkA'
- {_@_ `a{-s1fS-}' `tpl' `tpl'}
-`FF' ::
- `Boolean'
-`FF' =
- `FF'
- {}
-`TT' ::
- `Boolean'
-`TT' =
- `TT'
- {}
-`Nill' ::
- `LList alpha{-r3P-}'
-`Nill' =
- _/\_ `alpha{-s1fT-}' ->
- `Nill'
- {_@_ `alpha{-s1fT-}'}
-`Conss' ::
- `alpha{-r3P-} -> LList alpha{-r3P-} -> LList alpha{-r3P-}'
-`Conss' =
- _/\_ `alpha{-s1fU-}' -> \ `tpl' ::
- `alpha{-s1fU-}'
- `tpl' `tpl' ::
- `LList alpha{-s1fU-}'
- `tpl' ->
- `Conss'
- {_@_ `alpha{-s1fU-}' `tpl' `tpl'}
-Rec {
-`idl' ::
- `LList a{-aH5-} -> LList a{-aH5-}'
-`idl' =
- _/\_ `a{-s1fV-}' -> \ `xs' ::
- `LList a{-s1fV-}'
- `xs' ->
- case `xs' of {
- `Nill' ->
- `Nill'
- {_@_ `a{-s1fV-}'};
- `Conss' `y' `ys' ->
- let {
- `ds' ::
- `LList a{-s1fV-}'
- `ds' =
- `idl'
- _@_ `a{-s1fV-}' `ys'
- } in
- `Conss'
- {_@_ `a{-s1fV-}' `y' `ds'};
- }
-end Rec }
-`Zero' ::
- `Nat'
-`Zero' =
- `Zero'
- {}
-`Succ' ::
- `Nat -> Nat'
-`Succ' =
- \ `tpl' ::
- `Nat'
- `tpl' ->
- `Succ'
- {`tpl'}
-`Leaf' ::
- `x{-r3M-} -> Tree x{-r3M-}'
-`Leaf' =
- _/\_ `x{-s1fZ-}' -> \ `tpl' ::
- `x{-s1fZ-}'
- `tpl' ->
- `Leaf'
- {_@_ `x{-s1fZ-}' `tpl'}
-`Node' ::
- `Tree x{-r3M-} -> Tree x{-r3M-} -> Tree x{-r3M-}'
-`Node' =
- _/\_ `x{-s1g2-}' -> \ `tpl' ::
- `Tree x{-s1g2-}'
- `tpl' `tpl' ::
- `Tree x{-s1g2-}'
- `tpl' ->
- `Node'
- {_@_ `x{-s1g2-}' `tpl' `tpl'}
-`$d6' ::
- `{PrelBase.Eval Boolean}'
-`$d6' =
- `PrelBase.void'
-`$d3' ::
- `{PrelBase.Eval Nat}'
-`$d3' =
- `PrelBase.void'