df9ce10623
We can now write ``` @[init] def initFn : IO Unit := ... ``` instead of ``` def initFn : IO Unit := ... @[init initFn] constant execInitFn : Unit := () ```
27 lines
911 B
Text
27 lines
911 B
Text
import init.lean.options
|
|
|
|
open Lean
|
|
|
|
@[init] def initRegopt1 : IO Unit :=
|
|
registerOption `myNatOpt {defValue := DataValue.ofNat 0, descr := "my Nat option" }
|
|
|
|
@[init] def initRegopt2 : IO Unit :=
|
|
registerOption `myBoolOpt {defValue := DataValue.ofBool true, descr := "my Bool option" }
|
|
|
|
@[init] def initRegopt3 : IO Unit :=
|
|
registerOption `myStringOpt {defValue := DataValue.ofString "", descr := "my String option" }
|
|
|
|
@[init] def initRegopt4 : IO Unit :=
|
|
registerOption `myIntOpt {defValue := DataValue.ofInt 0, descr := "my Int option" }
|
|
|
|
|
|
def main : IO Unit :=
|
|
do getOptionDescr `myNatOpt >>= IO.println,
|
|
getOptionDescr `myBoolOpt >>= IO.println,
|
|
getOptionDescr `myIntOpt >>= IO.println,
|
|
let os : Options := {},
|
|
os ← setOptionFromString os "myNatOpt = 100",
|
|
IO.println (os.getNat `myNatOpt),
|
|
os ← setOptionFromString os "myIntOpt = -20",
|
|
IO.println (os.getInt `myIntOpt),
|
|
pure ()
|