28 lines
769 B
Text
28 lines
769 B
Text
import init.lean.evalconst
|
||
open Lean
|
||
|
||
def someVal := 100
|
||
def someVal2 : UInt64 := 302
|
||
def someVal3 : Bool := true
|
||
def add10 (n : Nat) := n+10
|
||
def mul10 (n : Nat) := n*10
|
||
def inc (n : Nat) := n+1
|
||
|
||
unsafe def evalNatFn (fName : Name) (n : Nat) : IO Unit :=
|
||
do f ← evalConst (Nat → Nat) fName,
|
||
IO.println (f n)
|
||
|
||
unsafe def evalVal (α : Type) [Inhabited α] [ToString α] (n : Name) : IO Unit :=
|
||
do v ← evalConst α n,
|
||
IO.println v
|
||
|
||
unsafe def main (xs : List String) : IO Unit :=
|
||
do let x := xs.head.toNat,
|
||
sortConstTable, -- we don't sort the constant table by default in standalone applications
|
||
evalNatFn `add10 x,
|
||
evalNatFn `mul10 x,
|
||
evalNatFn `inc x,
|
||
evalVal Nat `someVal,
|
||
evalVal UInt64 `someVal2,
|
||
evalVal Bool `someVal3,
|
||
pure ()
|