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
199 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: ...
2 votes
1 answer
176 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 ...
4 votes
1 answer
114 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: ...
1 vote
1 answer
69 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 ...
4 votes
2 answers
714 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 ...
1 vote
1 answer
82 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
238 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
382 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 ...