Opened 2 years ago
Definition proof step
|Reported by:||tilk||Owned by:|
One should be able to define his own constants in the proof. Defining set constants can currently be worked around by writing a lemma stating that the defined set exists, and then taking that set. One cannot define predicate constants now.
I would like to be able to write definitions like this:
P(x,y) <=> F
S = e
Where the defined constant doesn't occur in the definition (no recursion).
(Ticket moved from code.google.com)