Main project modules

• dui is in charge of the user interface, based on PySide2 (PyQt).

• server and lean are respectively the high-level and low-level interfaces with the Lean server.

• mathobj defines the class MathObject which stores mathematical objects, translate data from Lean into MathObject instances, and compute displayable versions of them.

• action translates the user's action on the user interface into Lean code.

• coursedata reads a Lean file and extracts a list of definitions, theorems and exercises from it.

The config.toml file

The file config.toml in src/share contains the factory settings. For instance the line

default_functionality_level = "Beginner"

indicates that the functionality level will be set to beginner when the user start using Deaduction. If the user changes this in the setting menu, then his choice will be savec in another config.toml` file, which is saved in $HOME/.deaduction . The values indicated in this second file override the factory settings.