some of the changes are backported from the hott3 library
pi_pathover and pi_pathover' are interchanged (same for variants and for sigma)
various definitions received explicit arguments: pinverse and eq_equiv_homotopy and ***.sigma_char
eq_of_fn_eq_fn is renamed to inj
in definitions about higher loop spaces and homotopy groups, the natural number arguments are now consistently before the type arguments
@avigad, @fpvandoorn, @rlewis1988, @dselsam
I changed how transitive instances are named.
The motivation is to avoid a naming collision problem found by Daniel.
Before this commit, we were getting an error on the following file
tests/lean/run/collision_bug.lean.
Now, transitive instances contain the prefix "_trans_".
It makes it clear this is an internal definition and it should not be used
by users.
This change also demonstrates (again) how the `rewrite` tactic is
fragile. The problem is that the matching procedure used by it has
very little support for solving matching constraints that involving type
class instances. Eventually, we will need to reimplement `rewrite`
using the new unification procedure used in blast.
In the meantime, the workaround is to use `krewrite` (as usual).
@avigad and @fpvandoorn, I changed the metaclasses names. They
were not uniform:
- The plural was used in some cases (e.g., [coercions]).
- In other cases a cryptic name was used (e.g., [brs]).
Now, I tried to use the attribute name as the metaclass name whenever
possible. For example, we write
definition foo [coercion] ...
definition bla [forward] ...
and
open [coercion] nat
open [forward] nat
It is easier to remember and is uniform.
@rlewis1988 We group all Lean constants used in the C++ code at
src/library/constants.txt
Jeremy and Floris check this file before renaming constants in the
library. So, they can quickly decide whether C++ code will be affected
or not.
We also have a python script for initializing the C++ name objects.
To use the script:
- go to src/library
- execute
python ../../script/gen_constants_cpp.py constants.txt
It will create the boring initialization and finalization code, and
declare a procedure get_<id>_name() for each constant in the file constants.txt.
I also move the norm_num1.lean to the set of unit tests that are
executed whenever we push a commit to the main branch.
I found an assertion violation at line 606. Could you take a look?
Best,
Leo
This is the correct fix for the id declaration pretty printing
discrepancy reported by Daniel.
TODO: decide whether we need another eq-mode where names are ignored.
For example, in blast, it makes sense to increase sharing by ignoring
binder names.
This renaming is because type_quotient is a nonstandard name. I've had a discussion with Egbert
Rijke, Steve Awodey and Dan Licata, and the consensus for a better name was 'quotient'. I had to
make changes in src/kernel/hits/hits.cpp, I renamed g_type_quotient* by g_hit_quotient* (to avoid
name clash the standard library quotient, although I don't know whether that name clash would
matter).
