It should be OK to use
_ instead of the original pattern when defining a function using
with. Example problem:
module Bug where data Foo : Set where foo : Foo f : Foo -> Foo f foo with foo f _ | foo = foo Bug.agda:7,1-8,18 With clause pattern _ is not an instance of its parent pattern when checking that the clause f foo with foo f _ | foo = foo has type Foo -> Foo
No it shouldn't.
Powered by PmWiki