All Questions
4
questions
11
votes
5
answers
2k
views
How do real-world proof assistants bind variables and check equality?
There are many possible ways to represent syntax with variable binding, such as named variables, De Bruijn indices, De Bruijn levels, locally nameless terms, nominal type theories, etc.
There are also ...
1
vote
1
answer
99
views
Applying universally quantified equalities to propositions
In Lean, given an equality eq: e0 = e1, one may rewrite either e0 or e1 with the other one ...
- 411
2
votes
1
answer
245
views
Is type checking in "Ideal Lean" computably enumerable?
There are actually two type theoretic foundations of Lean given in Mario Carneiro's master's thesis. They are the same, except for how definitional equality is treated:
“algorithmic” definitional ...
- 9,150
20
votes
2
answers
736
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? ...
- 410