blob: 0c3b35f693407bd1baaf5d4b676b74d8f38a58b1 [file] [edit]
---- Op
true
false
false
false
---- Foo 1
true
false
---- Foo 2
true
false
---- Op 2
false
true
false
false
---- Foo 3
match2.lean:83:0-85:21: error: the '(generalizing := true)' parameter is not supported when the 'match' motive is explicitly provided