Re: typecheck error

[John Rushby <RUSHBY@csl.sri.com>]

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


-------

---

• References:
  • typecheck error
    • From: "Gregory W. Kulczycki" <gregwk@cs.wvu.edu>

• Prev by Date: typecheck error
• Next by Date: Re: TYPE functions
• Prev by thread: typecheck error
• Next by thread: pvs error
• Index(es):
  • Date
  • Thread