5bd562b1d7da51cb5715899d32bb4c79c54459b0wrowevars a,b: Type

5bd562b1d7da51cb5715899d32bb4c79c54459b0wrowegenerated type Set a ::= empty | add a (Set a)

39021cf8b495cdb94013ca73531ccb32658fb793rederpjgenerated type Sys b ::= node b (Set (Sys b))

39021cf8b495cdb94013ca73531ccb32658fb793rederpj

39021cf8b495cdb94013ca73531ccb32658fb793rederpjtype Nat

39021cf8b495cdb94013ca73531ccb32658fb793rederpjvar a: Type

39021cf8b495cdb94013ca73531ccb32658fb793rederpjgenerated type CTree a ::= leaf a | branch (Nat ->? CTree a)

39021cf8b495cdb94013ca73531ccb32658fb793rederpj

39021cf8b495cdb94013ca73531ccb32658fb793rederpjfree type L ::= abs (L -> L)

39021cf8b495cdb94013ca73531ccb32658fb793rederpj

fa16f10bc02e46bc5a6c2c2c6371926cd1dbe2edwrowefree type Tree a b ::= leaf b | branch (a -> Tree a b)

fa16f10bc02e46bc5a6c2c2c6371926cd1dbe2edwrowe

fa16f10bc02e46bc5a6c2c2c6371926cd1dbe2edwrowefree type List a ::= nil | cons (a; List a)

fa16f10bc02e46bc5a6c2c2c6371926cd1dbe2edwrowe

fa16f10bc02e46bc5a6c2c2c6371926cd1dbe2edwrowefree type Tree a b ::= leaf a | branch (b -> List (Tree a b))

fa16f10bc02e46bc5a6c2c2c6371926cd1dbe2edwrowe

fa16f10bc02e46bc5a6c2c2c6371926cd1dbe2edwrowevar c : Type

fa16f10bc02e46bc5a6c2c2c6371926cd1dbe2edwroweop fold : (a -> c) -> ((b -> List c) -> c) -> Tree a b -> c

fa16f10bc02e46bc5a6c2c2c6371926cd1dbe2edwrowe

fa16f10bc02e46bc5a6c2c2c6371926cd1dbe2edwrowevars f : a -> c; g : (b -> List c) -> c; x : a; s : b -> List (Tree a b)

db8ac7cbb1fa6cdd6abcc4bb797d4deed32dd269jim. fold f g (leaf x) = f x

db8ac7cbb1fa6cdd6abcc4bb797d4deed32dd269jim. def (fold f g (branch s))

db8ac7cbb1fa6cdd6abcc4bb797d4deed32dd269jim