leanprover-community/batteries

`@[norm_cast move]` is broken

gebner opened this issue · 0 comments

gebner commented

The attribute elaborator checks whether move is a string literal, which it is not.