Questions tagged [errors]
Questions regarding software errors during the usage or development of Proof Assistants.
8
questions
0
votes
1
answer
337
views
An installation error in "Mathematics in Lean"
I have just started learning Lean 4 using Mathematics in Lean in Visual Studio Code, and I ran into a problem right away. I get the following error message:
...
CommunityBot
- 1
3
votes
1
answer
247
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 ...
- 9,653
4
votes
1
answer
124
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:
...
- 5,620
1
vote
1
answer
75
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 ...
- 5,620
3
votes
2
answers
756
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 ...
- 9,653
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 ...
- 9,653
5
votes
2
answers
264
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:
...
- 6,346
3
votes
2
answers
392
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 ...
- 9,653