Wolfram/LeanLink | Paclet Repository

Wolfram`LeanLink`

LeanEvaluate

LeanEvaluate ["expr"]
	evaluates the Lean expression expr with #eval and returns its value as a Wolfram Language expression.

Details and Options

▪

The value comes back through

Lean.toJson

:

Nat

and

Int

give integers,

Bool

gives

or

,

String

gives strings,

Float

gives machine reals, exactly, with

and

for the infinities and NaN, and

List

and

Array

give lists. A type without a

ToJson

instance fails; wrap the expression in

toString

to get a string instead.

▪

Options:

Option	Default
"ProjectDir"	None	a built Lake project whose modules the expression may use
"Imports"	{}	modules to import
"Source"	""	Lean declarations the expression uses (definitions, open s), placed after the imports
"Open"	{}	namespaces to open
"TimeLimit"	600	seconds before the evaluation is stopped