Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

error: aesop/linkProofs: internal error: reconstructed proof of goal 19 is type-incorrect #2

Closed
dselsam opened this issue Aug 7, 2021 · 1 comment

Comments

@dselsam
Copy link
Contributor

dselsam commented Aug 7, 2021

import Aesop.Main

inductive Even : Nat → Prop
| zero : Even Nat.zero
| plus_two {n} : Even n → Even (n + 2)

attribute [aesop safe] Even.zero Even.plus_two

example : Even 1000 := by aesop

gives

error: aesop/linkProofs: internal error: reconstructed proof of goal 19 is type-incorrect
@JLimperg
Copy link
Collaborator

Thanks! This was apparently already fixed in (my local) master.

JLimperg added a commit that referenced this issue Oct 5, 2021
This is the test case for issue #2 after all.
JLimperg pushed a commit that referenced this issue Oct 9, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants