fe77e4d2d1
This PR fixes a panic when `coinductive` predicates are defined inside macro scopes where constructor names carry macro scopes. The existing guard only checked the declaration name for macro scopes, missing the case where constructor identifiers are generated inside a macro quotation and thus carry macro scopes. This caused `removeFunctorPostfixInCtor` to panic on `Name.num` components from macro scope encoding. Closes #13415
13 lines
338 B
Text
13 lines
338 B
Text
macro "co " x:ident : command => do
|
|
`(coinductive $x : Prop where | ok)
|
|
|
|
/-- error: Coinductive predicates are not allowed inside of macro scopes -/
|
|
#guard_msgs in
|
|
co f
|
|
|
|
macro "co2" : command => do
|
|
`(coinductive test : Prop where | ctor)
|
|
|
|
/-- error: Coinductive predicates are not allowed inside of macro scopes -/
|
|
#guard_msgs in
|
|
co2
|