Axiom has a category structure (Axiom's kind, not the math kind).
The Axiom SANE branch is trying to structure definitions and axioms
to benefit from Lean's research.
In this paper, The Lean Mathematical Library
on page 4, there is a graph of the Lean structure hierarchy.
This differs considerably from Axiom's structure.
How can these work together? There is a bit of design issue here.
On the plus side, LEAN's structure has an underlying set of proofs.
We would really like to leverage this effort.
On the minus side, reorganizing Axiom's category hierarchy
to match this would undercut most of the existing code.
How to get the benefit and avoid the damage is currently
a major design consideration. At the moment I'm leaning
(pun intended) toward a parallel structure. Conceptually
that would mean that SANE would only explicitly reference
certain LEAN theorems directly and inherit the rest through
the LEAN structure. Unfortunately Axiom's category hierarchy
is somewhat ad-hoc and may not be strictly valid in some cases.
Research is SUCH fun :-)
Tim
LEANStructureHierarchy.png