Opened 4 years ago

#12 new enhancement

Definition proof step

Reported by: tilk Owned by:
Priority: major Component: Proof Engine
Version: Keywords:


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

Attachments (0)

Change History (0)

Add Comment

Modify Ticket

as new The ticket will remain with no owner.

E-mail address and user name can be saved in the Preferences.

Note: See TracTickets for help on using tickets.