All Questions
Tagged with type-checking lean3
2
questions
2
votes
1
answer
106
views
Why does an internal term produced by Lean's equation compiler have holes in it?
Section 4.7 of the Lean reference manual (version 3.3) gives an example of a division function defined by well-founded recursion. I used the #print command to ...
- 35
1
vote
1
answer
84
views
Code obtained from printing a definition from the Lean 3.46 equation compiler does not type check. Why doesn't it, and how can I fix it?
In the example below, the fibonacci function is defined via the Lean equation compiler. However, there seems to be a problem with the code that is obtained from running ...
- 35