lean3 icon indicating copy to clipboard operation
lean3 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

`tactic.copy_attribute`: local ==> permanent

Open leodemoura opened this issue 7 years ago • 0 comments

tactic.copy_attribute copies local attributes as permanent ones. To fix it, we need an API for checking whether an attribute is local or not. This bug is affecting transport_multiplicative_to_additive. See PR #1894

leodemoura avatar Dec 21 '17 16:12 leodemoura