max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: unsafe initialize

Browse source
This commit is contained in:
Sebastian Ullrich 2022-07-20 22:35:40 +02:00
parent b5417bdc6c
commit c43a84ca30
2 changed files with 6 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Lean/Elab/Declaration.lean
View file

@ -332,14 +332,12 @@ def elabMutual : CommandElab := fun stx => do
if let (some id, some type) := (id?, type?) then
let `(Parser.Command.declModifiersT| $[$doc?:docComment]? $[@[$attrs?,*]]? $(vis?)? $[unsafe%$unsafe?]?) := stx[0]
| Macro.throwErrorAt declModifiers "invalid initialization command, unexpected modifiers"
let declModifiers ← `(Parser.Command.declModifiersT| $[$doc?:docComment]? @[$attrId:ident initFn, $(attrs?.getD ∅),*] $(vis?)? $[unsafe%$unsafe?]?)
`(def initFn : IO $type := do $doSeq
$(⟨declModifiers⟩):declModifiers opaque $id : $type)
`($[unsafe%$unsafe?]? def initFn : IO $type := do $doSeq
$[$doc?:docComment]? @[$attrId:ident initFn, $(attrs?.getD ∅),*] $(vis?)? opaque $id : $type)
else
if let `(Parser.Command.declModifiersT| ) := declModifiers then
`(@[$attrId:ident] def initFn : IO Unit := do $doSeq)
else
Macro.throwErrorAt declModifiers "invalid initialization command, unexpected modifiers"
let `(Parser.Command.declModifiersT| ) := declModifiers
| Macro.throwErrorAt declModifiers "invalid initialization command, unexpected modifiers"
`(@[$attrId:ident] def initFn : IO Unit := do $doSeq)
| _ => Macro.throwUnsupported
builtin_initialize

1
tests/lean/run/unsafeInit.lean Normal file
View file

@ -0,0 +1 @@
unsafe initialize no : Nat ← pure lcUnreachable