Search code examples
typesisabelle

Isabelle Type Error

I am new to Isabelle and doing an Exercise for University. I need to proof a reverse function in Isabelle.

In Haskell the function would look like this:

rev [] = []
rev (x:xs) = rev xs ++ [x]

I now tryed to define this function "rev" in Isabelle. The type list and the function "app" (append)

function app and rev in Isabelle

The Error Isabelle gives me is:

Type unification failed: Clash of types "_
          ⇒ _" and "_ Exercise5.list"

Type error in application: incompatible operand type

Operator:  app (rev xs) ::
  'a Exercise5.list ⇒ 'a Exercise5.list
Operand:   Exercise5.list.Cons ::
  ??'a ⇒ ??'a Exercise5.list ⇒ ??'a Exercise5.list

Where is the Problem? As far as I understand it Isabelle is telling me "Hey buddy app needs 2 arguments of type a' list but this is not the case here"

but why? xs is clearly of type a' list and with my Cons operator i do make x also a list?

Thanks for the Help!

Solution

  • Think about where the parenthesis should be put in app rev xs Cons x Nil: Currently you seem to apply the function x on its argument Nil.