Haskell

Please enter a (polymorphic) type, e.g. "(a -> Bool) -> [a] -> [a]" or simply "filter":

Please choose a sublanguage of Haskell:

no bottoms (hence no general recursion and no selective strictness)

general recursion but no selective strictness

general recursion and selective strictness

Please choose a theorem style (without effect in the sublanguage with no bottoms):

equational

inequational

If you need additional declarations you can enter them here: