Beta version

To access the latest (unstable!) version, open a Terminal, go to the deaduction directory, and type

git pull
git checkout develop

Beware that the names of the course files may have changed: use "Browse files for courses" to find the new files.

New features in beta version

• A proof outline window.
• An "equal" button, a "maps to" button, no "Apply" button.
• A menu, with access to settings.
• The order in which the objects are selected does not affect the action.
• The geometry of the exercise window is saved and restored at the next session
• File extension is now '.lean', instead of '.pkl' (the information that was previously stored in the .pklfiles is now computed live the first time a .lean file is opened, and stored silently).
• Use of implicit definitions : e.g. button "AND" will work on an expression like x∈A∩B, and the property f is injectivewill be recognize as a universal implication by buttons "FOR ALL" and "IMPLIES".
• Several bugs corrected in the exercise chooser window.
• New way of naming variables. In particular, the default setting is that dummy variables cannot have the same name as a variable in the context.
• "Goal!" button is far more efficient than before.
• variables are now in color: context variables in blue, and dummy variables in purple. This uses html-like display. the display have been modified, and the text display in the chooser should be better.
• Possibility to automatically apply existence hypotheses to get a new object (in settings).
• Possibility to change font size