Questions tagged [errors]

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

Filter by
Sorted by
Tagged with
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 ...
Nate Glenn's user avatar
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 ...
Nate Glenn's user avatar
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 ...
Nate Glenn's user avatar
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: ...
noCrayCray's user avatar
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 ...
ttbo's user avatar
  • 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: ...
IsAdisplayName's user avatar
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 ...
taylor.2317's user avatar
  • 1,308