Questions tagged [errors]
Questions regarding software errors during the usage or development of Proof Assistants.
7
questions
1
vote
1
answer
69
views
Recursive type class for OfNat Even
I'm working my way through Functional Programming in Lean. There's an exercise to create an Even class to represent even natural numbers.
I was able to define ...
- 197
1
vote
1
answer
53
views
Typing List.nil
I'm working my way through Functional Programming in Lean and there's an exercise to create a zip function for combining two ...
- 197
3
votes
2
answers
622
views
proof of termination for zip in Lean
I'm making my way through Functional Programming in Lean and there's an exercise to implement zip, which takes two lists and returns a list of tuples the length of ...
- 197
3
votes
1
answer
69
views
"Expected a single focused goal but 2 goals are focused." error in coq regarding string equality(I think)
I'm working through Software Foundations, I'm at "Maps" right now. There's an exercise:
...
- 51
1
vote
1
answer
78
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
5
votes
2
answers
198
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:
...
- 305
3
votes
2
answers
350
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 ...
- 1,308