Andromedans / andromeda

A proof assistant for general type theories
http://www.andromeda-prover.org/
Other
297 stars 34 forks source link

Introduce the `a ≡ b : T by p` and `A ≡ B by q` notations. #504

Closed andrejbauer closed 4 years ago

andrejbauer commented 4 years ago

These are equivalent to p :? (a ≡ b : T by ??) and q :? (A ≡ B by ??), respectively. And they are very logical and nice to have.