Undefined atoms

[David Baelde]

Hi list,

Is there any way to declare undefined atoms in Abella?

For now, what I'm doing is declaring a predicate symbol in the sig, not attaching any clause in the mod. Then, I can define atom a in the thm do mean {a}, but when using it I have to be careful not to do any case analysis on it.

Is there a better way?

Thanks,

David

[David Baelde]

Thanks Kaustuv for the solution:

The declaration can be done using
Type foo prop.

Or in my case:
Type lt_a lfobj -> lfobj -> prop.

David