issues
search
Andromedans
/
andromeda
A proof assistant for general type theories
http://www.andromeda-prover.org/
Other
297
stars
34
forks
source link
Improve the `eq` module
#512
Open
andrejbauer
opened
4 years ago
andrejbauer
commented
4 years ago
Make it possible to install immediate equations (maybe both, normalized and non-normalized)
There should be a way to locally use an equation.
There should be a way to block an equation that's already installed.
It would be nice if we can have multiple equality checkers at the same time, apart from the default one.