Skip to content

Commit 09b011d

Browse files
Jlh18digama0
andauthored
chore: switch Id definition (#135)
* switch Id definition * fix --------- Co-authored-by: Mario Carneiro <di.gama@gmail.com>
1 parent cb6c77c commit 09b011d

File tree

3 files changed

+226
-222
lines changed

3 files changed

+226
-222
lines changed

GroupoidModel/ForMathlib/CategoryTheory/Yoneda.lean

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -8,20 +8,20 @@ notation:max "y(" Γ ")" => yoneda.obj Γ
88
notation:max "ym(" f ")" => yoneda.map f
99

1010
open Lean PrettyPrinter in
11-
@[app_unexpander Prefunctor.obj]
12-
def Prefunctor.obj.unexpand : Unexpander
11+
@[app_unexpander Functor.obj]
12+
def Functor.obj.unexpand : Unexpander
1313
| `($_ $F $X) =>
14-
if let .node _ _ #[.ident _ _ `yoneda _, _, .ident _ _ `toPrefunctor _] := F.raw then
14+
if let .ident _ _ `yoneda _ := F.raw then
1515
`(y($X))
1616
else
1717
throw ()
1818
| _ => throw ()
1919

2020
open Lean PrettyPrinter in
21-
@[app_unexpander Prefunctor.map]
22-
def Prefunctor.map.unexpand : Unexpander
21+
@[app_unexpander Functor.map]
22+
def Functor.map.unexpand : Unexpander
2323
| `($_ $F $X) =>
24-
if let .node _ _ #[.ident _ _ `yoneda _, _, .ident _ _ `toPrefunctor _] := F.raw then
24+
if let .ident _ _ `yoneda _ := F.raw then
2525
`(ym($X))
2626
else
2727
throw ()

0 commit comments

Comments
 (0)