Questions tagged [errors]
Questions regarding software errors during the usage or development of Proof Assistants.
3
questions
1
vote
1
answer
65
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 ...
5
votes
2
answers
174
views
Agda: Cannot Instantiate Metavariable
I'm running into a certain error while trying to code something up in cubical Agda, but I can't understand the error. Here is my code:
...
3
votes
2
answers
313
views
How do you know a formal proof (mechanized within a Proof Assistant) really is correct?
Running a proof assistant as a user and focusing on a given formal proof, how can one assert that there are no unexpected errors or "bugs" that could invalidate the provided proof?
More ...