[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: typecheck error



Gregory Kulczycki gets a typecheck error about = from
    o_empty2: THEOREM empty_seq o a = a

The problem is actually in determining the type of empty_seq
If you make this explicit with
    o_empty2: THEOREM empty_seq[T] o a = a
Then the problem goes away (and you can prove the theorem in five commands).

Alternatively, you could explicitly import the specific theory instance with
 IMPORTING finite_sequences[T]
and then drop all subsequent mention of [T]

John


-------