Questions tagged [equality]
Questions pertaining to equality in type theory (all kinds of equality are included: judgemental, propositional, observational, setoid equality, etc.) and equality reasoning in proof assistants.
32
questions
11
votes
1
answer
543
views
How does Metamath Zero handle CIC as in Lean or Coq?
Metamath Zero (MM0) is a proof assistant developed by Mario Carneiro. It has a metalogic very similar to the metalogic of MetaMath, but it also borrows design choices from Lean (and maybe other ...
- 1,599
20
votes
2
answers
745
views
What is the difference between refl and rfl in Lean 3?
I already know that refl is called a tactic, and that rfl is a term; can you explain with examples how they technically differ? ...
- 731