1
module tests.Mutual where
4
open import Prelude.String
5
open import Prelude.Unit
9
GA : {g : G}(f : F g) -> G
12
data F : G -> Set where
19
incG (GA f) = GA (incF f)
21
incF : {g : G} -> F g -> F (incG g)
23
incF (FA g) = FA (incG g)
29
PrintF : {g : G} -> F g -> String
31
PrintF (FA g) = "(FA " +S+ PrintG g +S+ ")"
35
PrintG (GA f) = "(GA " +S+ PrintF f +S+ ")"
39
putStrLn (PrintF (FA (GA (FA GB)))) ,,
40
putStrLn (PrintG (incG (GA (incF FB)))) ,, --
b'\\ No newline at end of file'