search

vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
302 stars 52 forks source link

raise USER_ERROR on undeclared type constructor #611

Closed MichaelRawson closed 2 months ago

MichaelRawson commented 2 months ago

@quickbeam123 - refer e-mail chain with Geoff. Now raises an error if a TFF type constructor is used before it is declared.

Minimal example:

% tff(set_type, type, set : $tType).
tff(member_type, type, member : set).