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 56ab5d3 commit 7106388Copy full SHA for 7106388
Batteries/Tactic/Alias.lean
@@ -87,7 +87,9 @@ 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
- computeKind := if isNoncomputable (← getEnv) name then .noncomputable else declMods.computeKind
+ computeKind :=
91
+ if isNoncomputable (← getEnv) name then .noncomputable
92
+ else declMods.computeKind
93
isUnsafe := declMods.isUnsafe || cinfo.isUnsafe
94
attrs
95
}
0 commit comments