Daniel Fabian (Mar 13 2021 at 20:13):
I'm trying out lean 4 and I'm getting an error in a pattern that I thought should work:
inductive color | red | black inductive node where | leaf : node | tree (color : color) : node def balance : color → node → node -- the following line fails with: invalid pattern variable, must be atomic | color.red, node.tree color.red => node.leaf -- the following line works fine --| color.red, node.tree anyColor => node.leaf | _, _ => node.leaf
Any idea why this doesn't work?
Julian Berman (Mar 13 2021 at 21:37):
This seems to work for me (well produce no errors at least) on
Lean (version 4.0.0-nightly-2021-03-13, commit 472c5fb900ea, Release)
Daniel Fabian (Mar 13 2021 at 22:40):
indeed, when I updated lean4, I no longer get the error, so it must have been fixed recently. Interesting.
Last updated: May 07 2021 at 12:15 UTC