diff options
Diffstat (limited to 'transfer/examples/widesnake.tra')
| -rw-r--r-- | transfer/examples/widesnake.tra | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/transfer/examples/widesnake.tra b/transfer/examples/widesnake.tra new file mode 100644 index 000000000..e27bd5981 --- /dev/null +++ b/transfer/examples/widesnake.tra @@ -0,0 +1,19 @@ +import bool +import stoneage + +monoid_Bool : sig { zero : Bool; plus : Bool -> Bool -> Bool } +monoid_Bool = rec + zero = False + plus = \x -> \y -> x && y + +isSnake : (A : Tree) -> Tree A -> Bool +isSnake _ x = case x of + Snake -> True + _ -> composFold ? ? compos_Tree Bool monoid_Bool ? isSnake x + +wideSnake : (A : Cat) -> Tree A -> Tree A +wideSnake _ x = case x of + Wide y -> let y' : CN = wideSnake ? y + in if isSnake CN y' then Thick y' else Wide y' + _ -> composOp ? ? compos_Tree ? wideSnake x + |
