A bi-directional extensible ad hoc interface between Lean and Mathematica

Supplementary Materials

These materials correspond to this paper. For more information, contact Robert Y. Lewis and Minchao Wu.

Versioning

All code and examples are designed for Lean 3.3.0. One set of examples requires a modified version of Lean 3.3.0, described below.

Installing the link

The code for using Mathematica from Lean is available on Github. This project can be added as a dependency to any Lean project using the leanpkg package manager.

To use the link in this direction, you must start the Mathematica server. Do this either by

  1. Running math --noprompt -run "<<server2.m" in the directory containing the above project, or
  2. Opening the Mathematica frontend and running <<"server2.m" (with the correct path)

The code for using Lean from Mathematica is also available on Github. This project uses the above as a dependency.

To use the link in this direction, run leanpkg build in the root directory, and open MathematicaExamples.nb. The relevance filter examples currently require a customized version of Lean, which you can download and build here. (The customized version of Lean allows computations with floats in Lean's meta language; it does not affect soundness in any way.)

Possible Issues

The Mathematica-from-Lean link expects a python2 executable in the path. Create an alias if you do not have this.

The link communicates over port 10000. If this is taken, change the port numbers in client2.py and server2.m.

There are known issues with Mathematica's socket server functionality on certain versions of Linux. This may cause the server to use excess CPU.

The Lean-from-Mathematica link requires you to set the Mathematica directory to the lean_mm root.

If you are not running the customized version of Lean allowing float computation, you will see some warning messages when building the mm_lean project. These can safely be ignored.

A minor namespacing bug causes unnecessary import clashes. These create warning messages on the relevance filter examples, which can safely be ignored.

Examples of the link

A project containing examples of the Mathematica-from-Lean link in action is available here.

The file MathematicaExamples.nb in the mm_lean project contains examples of the Lean-from-Mathematica link.

Additional information

The full, unabbreviated form of the expression x^2-2*x+1 in Lean is

app (app (app (app (const (name.mk_string add (name.anonymous)) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_has_add (name.mk_string distrib (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_distrib (name.mk_string ring (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_ring (name.mk_string division_ring (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_division_ring (name.mk_string field (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_field (name.mk_string linear_ordered_field (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (const (name.mk_string h (name.anonymous)) (level_list.nil)))))))) (app (app (app (app (const (name.mk_string sub (name.anonymous)) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string add_group_has_sub (name.anonymous)) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_add_group (name.mk_string add_comm_group (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_add_comm_group (name.mk_string ring (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_ring (name.mk_string division_ring (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_division_ring (name.mk_string field (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_field (name.mk_string linear_ordered_field (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (const (name.mk_string h (name.anonymous)) (level_list.nil))))))))) (app (app (app (app (const (name.mk_string mul (name.anonymous)) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_has_mul (name.mk_string mul_zero_class (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_mul_zero_class (name.mk_string semiring (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_semiring (name.mk_string ordered_semiring (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_ordered_semiring (name.mk_string ordered_ring (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_ordered_ring (name.mk_string linear_ordered_ring (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_linear_ordered_ring (name.mk_string linear_ordered_field (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (const (name.mk_string h (name.anonymous)) (level_list.nil))))))))) (local_const (name.mk_numeral 1 (name.mk_numeral 18 (name.anonymous))) (name.mk_string x (name.anonymous)) (binder_info.default) (const (name.mk_string real (name.anonymous)) (level_list.nil)))) (local_const (name.mk_numeral 1 (name.mk_numeral 18 (name.anonymous))) (name.mk_string x (name.anonymous)) (binder_info.default) (const (name.mk_string real (name.anonymous)) (level_list.nil))))) (app (app (app (app (const (name.mk_string mul (name.anonymous)) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_has_mul (name.mk_string mul_zero_class (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_mul_zero_class (name.mk_string semiring (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_semiring (name.mk_string ordered_semiring (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_ordered_semiring (name.mk_string ordered_ring (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_ordered_ring (name.mk_string linear_ordered_ring (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_linear_ordered_ring (name.mk_string linear_ordered_field (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (const (name.mk_string h (name.anonymous)) (level_list.nil))))))))) (app (app (app (const (name.mk_string bit0 (name.anonymous)) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_has_add (name.mk_string distrib (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_distrib (name.mk_string ring (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_ring (name.mk_string division_ring (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_division_ring (name.mk_string field (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_field (name.mk_string linear_ordered_field (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (const (name.mk_string h (name.anonymous)) (level_list.nil)))))))) (app (app (const (name.mk_string one (name.anonymous)) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_has_one (name.mk_string zero_ne_one_class (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_zero_ne_one_class (name.mk_string division_ring (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_division_ring (name.mk_string field (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_field (name.mk_string linear_ordered_field (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (const (name.mk_string h (name.anonymous)) (level_list.nil))))))))) (local_const (name.mk_numeral 1 (name.mk_numeral 18 (name.anonymous))) (name.mk_string x (name.anonymous)) (binder_info.default) (const (name.mk_string real (name.anonymous)) (level_list.nil)))))) (app (app (const (name.mk_string one (name.anonymous)) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_has_one (name.mk_string zero_ne_one_class (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_zero_ne_one_class (name.mk_string division_ring (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_division_ring (name.mk_string field (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (app (app (const (name.mk_string to_field (name.mk_string linear_ordered_field (name.anonymous))) (level_list.cons (level.zero) (level_list.nil))) (const (name.mk_string real (name.anonymous)) (level_list.nil))) (const (name.mk_string h (name.anonymous)) (level_list.nil)))))))

The Mathematica version of this same expression is:

"LeanApp[LeanApp[LeanApp[LeanApp[LeanConst[LeanNameMkString["add", LeanNameAnonymous], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_has_add", LeanNameMkString["distrib", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_distrib", LeanNameMkString["ring", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_ring", LeanNameMkString["division_ring", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_division_ring", LeanNameMkString["field", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_field", LeanNameMkString["linear_ordered_field", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanConst[LeanNameMkString["h", LeanNameAnonymous], LeanLevelListNil]]]]]]], LeanApp[LeanApp[LeanApp[LeanApp[LeanConst[LeanNameMkString["sub", LeanNameAnonymous], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["add_group_has_sub", LeanNameAnonymous], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_add_group", LeanNameMkString["add_comm_group", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_add_comm_group", LeanNameMkString["ring", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_ring", LeanNameMkString["division_ring", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_division_ring", LeanNameMkString["field", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_field", LeanNameMkString["linear_ordered_field", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanConst[LeanNameMkString["h", LeanNameAnonymous], LeanLevelListNil]]]]]]]], LeanApp[LeanApp[LeanApp[LeanApp[LeanConst[LeanNameMkString["mul", LeanNameAnonymous], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_has_mul", LeanNameMkString["mul_zero_class", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_mul_zero_class", LeanNameMkString["semiring", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_semiring", LeanNameMkString["ordered_semiring", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_ordered_semiring", LeanNameMkString["ordered_ring", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_ordered_ring", LeanNameMkString["linear_ordered_ring", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_linear_ordered_ring", LeanNameMkString["linear_ordered_field", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanConst[LeanNameMkString["h", LeanNameAnonymous], LeanLevelListNil]]]]]]]], LeanLocal[LeanNameMkNum[1843, LeanNameMkNum[17, LeanNameAnonymous]], LeanNameMkString["x", LeanNameAnonymous], BinderInfoDefault, LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]]], LeanLocal[LeanNameMkNum[1843, LeanNameMkNum[17, LeanNameAnonymous]], LeanNameMkString["x", LeanNameAnonymous], BinderInfoDefault, LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]]]], LeanApp[LeanApp[LeanApp[LeanApp[LeanConst[LeanNameMkString["mul", LeanNameAnonymous], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_has_mul", LeanNameMkString["mul_zero_class", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_mul_zero_class", LeanNameMkString["semiring", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_semiring", LeanNameMkString["ordered_semiring", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_ordered_semiring", LeanNameMkString["ordered_ring", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_ordered_ring", LeanNameMkString["linear_ordered_ring", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_linear_ordered_ring", LeanNameMkString["linear_ordered_field", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanConst[LeanNameMkString["h", LeanNameAnonymous], LeanLevelListNil]]]]]]]], LeanApp[LeanApp[LeanApp[LeanConst[LeanNameMkString["bit0", LeanNameAnonymous], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_has_add", LeanNameMkString["distrib", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_distrib", LeanNameMkString["ring", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_ring", LeanNameMkString["division_ring", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_division_ring", LeanNameMkString["field", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_field", LeanNameMkString["linear_ordered_field", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanConst[LeanNameMkString["h", LeanNameAnonymous], LeanLevelListNil]]]]]]], LeanApp[LeanApp[LeanConst[LeanNameMkString["one", LeanNameAnonymous], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_has_one", LeanNameMkString["zero_ne_one_class", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_zero_ne_one_class", LeanNameMkString["division_ring", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_division_ring", LeanNameMkString["field", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_field", LeanNameMkString["linear_ordered_field", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanConst[LeanNameMkString["h", LeanNameAnonymous], LeanLevelListNil]]]]]]]], LeanLocal[LeanNameMkNum[1843, LeanNameMkNum[17, LeanNameAnonymous]], LeanNameMkString["x", LeanNameAnonymous], BinderInfoDefault, LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]]]]], LeanApp[LeanApp[LeanConst[LeanNameMkString["one", LeanNameAnonymous], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_has_one", LeanNameMkString["zero_ne_one_class", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_zero_ne_one_class", LeanNameMkString["division_ring", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_division_ring", LeanNameMkString["field", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanApp[LeanApp[LeanConst[LeanNameMkString["to_field", LeanNameMkString["linear_ordered_field", LeanNameAnonymous]], LeanLevelListCons[LeanZeroLevel, LeanLevelListNil]], LeanConst[LeanNameMkString["real", LeanNameAnonymous], LeanLevelListNil]], LeanConst[LeanNameMkString["h", LeanNameAnonymous], LeanLevelListNil]]]]]]]