We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 7547d99 commit 56ab5d3Copy full SHA for 56ab5d3
Batteries/Tactic/Alias.lean
@@ -87,7 +87,7 @@ elab (name := alias) mods:declModifiers "alias " alias:ident " := " name:ident :
87
let declMods ← elabModifiers mods
88
let (attrs, machineApplicable) := setDeprecatedTarget name declMods.attrs
89
let declMods := { declMods with
90
- isNoncomputable := declMods.isNoncomputable || isNoncomputable (← getEnv) name
+ computeKind := if isNoncomputable (← getEnv) name then .noncomputable else declMods.computeKind
91
isUnsafe := declMods.isUnsafe || cinfo.isUnsafe
92
attrs
93
}
0 commit comments