module test

import StdEnv

:: Z = Z
:: S a = S a

class peano a :: a
instance peano Z where peano = Z
instance peano (S a) | peano a where peano = S peano

class peanoplus a b ~c
where
	peanoplus :: a b -> c

instance peanoplus a Z a | peano a
where
	peanoplus a b = a

:: FString n = FS [Char]

fsempty :: FString Z
fsempty = FS []

fappend :: (FString a) Char -> FString (S a) | peano a
fappend (FS l) c = FS (l ++ [c])

Start = peanoplus Z Z