Skip to main content

Questions tagged [errors]

Questions regarding software errors during the usage or development of Proof Assistants.

Filter by
Sorted by
Tagged with
0 votes
1 answer

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: ...
1 vote
1 answer

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 ...
4 votes
1 answer

"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: ...
1 vote
1 answer

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 ...
4 votes
2 answers

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 ...
1 vote
1 answer

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

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

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 ...