Skip to content

Commit

Permalink
enableInitializersExecution
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em committed Feb 14, 2025
1 parent bce849f commit e719eea
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions scripts/declaration_types.lean
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ def Lean.ConstantInfo.kind : ConstantInfo → String
| .recInfo _ => "recursor"

def main (args : List String) : IO UInt32 := do
unsafe enableInitializersExecution
let modules := match args with
| [] => #[`Mathlib]
| args => args.toArray.map fun s => s.toName
Expand Down

0 comments on commit e719eea

Please sign in to comment.