batteries icon indicating copy to clipboard operation
batteries copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

`@[norm_cast move]` is broken

Open gebner opened this issue 2 years ago • 0 comments

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

gebner avatar Jan 08 '23 02:01 gebner