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
129 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: ...
Blankino's user avatar
1 vote
1 answer
136 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 ...
Nate Glenn's user avatar
1 vote
1 answer
59 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 ...
Nate Glenn's user avatar
4 votes
2 answers
696 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 ...
Nate Glenn's user avatar
4 votes
1 answer
101 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: ...
noCrayCray's user avatar
1 vote
1 answer
80 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 ...
ttbo's user avatar
  • 35
5 votes
2 answers
229 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: ...
IsAdisplayName's user avatar
3 votes
2 answers
380 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 ...
taylor.2317's user avatar
  • 1,308