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.

Sign up for GitHub

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

Jump to bottom

Some tactics fail if traverse function is anonymous #8

Open
KevOrr opened this issue Sep 25, 2019 · 0 comments
Open

Some tactics fail if traverse function is anonymous #8

KevOrr opened this issue Sep 25, 2019 · 0 comments
Assignees
@KevOrr
Labels
bug

Comments

@KevOrr
Copy link
Member

KevOrr commented Sep 25, 2019 •
edited
Loading

E.g.

Inductive term : Set :=
| ...
.

Instance Traverse_term : Traverse term term :=
  {traverse := (fix rec f l e := ...)}.

Goal @TraverseFunctorial term _ term _.
Proof.
  constructor. prove_traverse_functorial.

Shown to break:

  • prove_traverse_functorial
  • prove_traverse_relative
  • prove_traverse_var_is_identity

Shown to work:

  • prove_traverse_var_injective
  • prove_traverse_identifies_var
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@KevOrr KevOrr

Labels
bug
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@KevOrr