Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
LeanExport  |
| |
Examples
(1)
Properties & Relations
(1)
is followed by a write: writes the same text that returns.
 |
|
 |
|
Export an environment to a temporary file: The file now exists on disk: Read the first line back:
.lean
In[1]:=
env=
["theorem myT : Nat.succ 0 = 1 := rfl"];file=
[FileNameJoin[{$TemporaryDirectory,"out.lean"}],env]
 | LeanImportString |
 | LeanExport |
Out[1]=
/private/var/folders/5x/lyq7cw110cx_zr1zb3zr63gm0000gn/T/out.lean
In[2]:=
FileExistsQ[file]
Out[2]=
True
In[3]:=
First@StringSplit[Import[file,"Text"],""]
Out[3]=
theorem myT : (Nat.succ (OfNat.ofNat Nat 0 (instOfNatNat 0))) = (OfNat.ofNat Nat 1 (instOfNatNat 1)) := sorry
""