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

derive monad #1951

Closed
fpvandoorn opened this issue Feb 4, 2020 · 0 comments
Closed

derive monad #1951

fpvandoorn opened this issue Feb 4, 2020 · 0 comments
Labels
bug

Comments

@fpvandoorn
Copy link
Member

In this code snippet

import tactic

@[derive monad] 
meta def my_tactic : Type → Type :=
tactic

The derive handler assumes that I want the instance monad (my_tactic a) instead of monad my_tactic
@fpvandoorn fpvandoorn added the bug label Feb 4, 2020
@robertylewis robertylewis mentioned this issue Apr 21, 2020
Closed
7 tasks
bors bot pushed a commit that referenced this issue Apr 23, 2020
@robertylewis
feat(tactic/delta_instance): protect names and deal with functions (#…
8eb74b9 
…2477)

There were (at least) two issues with the `delta_instance` derive handler:
* It couldn't protect the names of the instances it generated, so they had to be ugly to avoid clashes.
* It didn't deal well with deriving instances on function types, so `@[derive monad]` usually failed.

This should fix both. The first is possible with recent(ish) additions to core.

closes #1951



Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
bors bot pushed a commit that referenced this issue Apr 24, 2020
@robertylewis
feat(tactic/delta_instance): protect names and deal with functions (#…
174d479 
…2477)

There were (at least) two issues with the `delta_instance` derive handler:
* It couldn't protect the names of the instances it generated, so they had to be ugly to avoid clashes.
* It didn't deal well with deriving instances on function types, so `@[derive monad]` usually failed.

This should fix both. The first is possible with recent(ish) additions to core.

closes #1951



Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
@bors bors bot closed this as completed in 3162c1c Apr 24, 2020
anrddh pushed a commit to anrddh/mathlib that referenced this issue May 15, 2020
@robertylewis @anrddh
feat(tactic/delta_instance): protect names and deal with functions (l…
eb101a9 
…eanprover-community#2477)

There were (at least) two issues with the `delta_instance` derive handler:
* It couldn't protect the names of the instances it generated, so they had to be ugly to avoid clashes.
* It didn't deal well with deriving instances on function types, so `@[derive monad]` usually failed.

This should fix both. The first is possible with recent(ish) additions to core.

closes leanprover-community#1951



Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
anrddh pushed a commit to anrddh/mathlib that referenced this issue May 16, 2020
@robertylewis @anrddh
feat(tactic/delta_instance): protect names and deal with functions (l…
4580edc 
…eanprover-community#2477)

There were (at least) two issues with the `delta_instance` derive handler:
* It couldn't protect the names of the instances it generated, so they had to be ugly to avoid clashes.
* It didn't deal well with deriving instances on function types, so `@[derive monad]` usually failed.

This should fix both. The first is possible with recent(ish) additions to core.

closes leanprover-community#1951



Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
cipher1024 pushed a commit to cipher1024/mathlib that referenced this issue Mar 15, 2022
@robertylewis @cipher1024
feat(tactic/delta_instance): protect names and deal with functions (l…
c9f10b8 
…eanprover-community#2477)

There were (at least) two issues with the `delta_instance` derive handler:
* It couldn't protect the names of the instances it generated, so they had to be ugly to avoid clashes.
* It didn't deal well with deriving instances on function types, so `@[derive monad]` usually failed.

This should fix both. The first is possible with recent(ish) additions to core.

closes leanprover-community#1951



Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug
Projects
None yet
Milestone
No milestone
1 participant
@fpvandoorn