Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Wolfram`LeanLink`
LeanExportString  |
| | |||||
▪
Each constant is emitted as a Lean declaration of its type: a theorem as a , an axiom as an , and any other constant, definition, inductive type or constructor, as a . The constants come in an order where each follows those its type names.
theorem
axiom
def
▪
A constant imported from compiled data has no body that can be written back, so its body is , and its type is exported exactly: every constant applied with and every argument written, implicit ones included, raw literals as , and each bound variable named by its binder, renamed where that name is taken. Compiled again, the source declares the same constants with the same types.
.olean
sorry
@
nat_lit
▪
An environment produced by carries structured tactic proofs, which export as faithful blocks.
:=by...
▪
Examples
(3)
Basic Examples
(1)
In[1]:=
leanEnv=
[FindEquationalProof[ac,{ab,bc}]]
 | ProofToLean |
Out[1]=
LeanEnvironment
 |
|
In[2]:=
 | LeanExportString |
Out[2]=
axiom U : Typeaxiom Ax1 : ∀ (b : U) (a : U), b = aaxiom Ax2 : ∀ (b : U) (c : U), b = caxiom Hyp1 : ∀ (a : U) (c : U), a = ctheorem SL1 : ∀ (a : U) (c : U), a = c := by intro a c have h := Ax2 a c conv at h => lhs; simp only [Ax1] exact htheorem FinalGoal : ∀ (a : U) (c : U), a = c := by intro a c exact SL1 a c
Scope
(1)
Properties & Relations
(1)
 |
|
 |
|
""