Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
LeanExportString  |
| |
Examples
(2)
Scope
(1)
Exporting an imported environment renders each declaration's type, with standing in for bodies that are not reconstructible from compiled data:
sorry
In[1]:=
env=
["theorem myT : Nat.succ 0 = 1 := rfl"];
[env]
 | LeanImportString |
 | LeanExportString |
Out[1]=
theorem myT : (Nat.succ (OfNat.ofNat Nat 0 (instOfNatNat 0))) = (OfNat.ofNat Nat 1 (instOfNatNat 1)) := sorry
Properties & Relations
(1)
 |
|
 |
|
In[1]:=
leanEnv=
[FindEquationalProof[ac,{ab,bc}]];
[leanEnv]
| ProofToLean |
| LeanExportString |
Out[1]=
axiom U : Typeaxiom Ax1 : b = aaxiom Ax2 : b = caxiom Hyp1 : a = ctheorem SL1 : a = c := by have h := Ax2 conv at h => lhs; simp only [Ax1] exact htheorem FinalGoal : a = c := by exact SL1
""