Texte vergleichen

Finden Sie den Unterschied zwischen zwei Textdateien

Real-time diff

Unified diff

Collapse lines

Highlight change

Syntax highlighting

Onlinewerkzeuge

Diffchecker Desktop The most secure way to run Diffchecker. Get the Diffchecker Desktop app: your diffs never leave your computer!Get Desktop

Foo

Created 6 months agoDiff never expires

329 lines

[result]

def _private.tests.lean.run.toFromJson.0.toJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1421._closed_1 : obj :=

def _private.lean.run.toFromJson.0.toJsonFoo.«_@».lean.run.toFromJson._hyg.1421._closed_1 : obj :=

let x_1 : obj := "x";

ret x_1

def _private.tests.lean.run.toFromJson.0.toJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1421._closed_2 : obj :=

def _private.lean.run.toFromJson.0.toJsonFoo.«_@».lean.run.toFromJson._hyg.1421._closed_2 : obj :=

let x_1 : obj := "y";

ret x_1

def _private.tests.lean.run.toFromJson.0.toJsonFoo._@.tests.lean.run.toFromJson._hyg.1421 (x_1 : obj) : obj :=

def _private.lean.run.toFromJson.0.toJsonFoo._@.lean.run.toFromJson._hyg.1421 (x_1 : obj) : obj :=

let x_2 : obj := proj[0] x_1;

inc x_2;

let x_3 : obj := Lean.JsonNumber.fromNat x_2;

let x_4 : obj := ctor_2[Lean.Json.num] x_3;

let x_5 : obj := _private.tests.lean.run.toFromJson.0.toJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1421._closed_1;

let x_5 : obj := _private.lean.run.toFromJson.0.toJsonFoo.«_@».lean.run.toFromJson._hyg.1421._closed_1;

let x_6 : obj := ctor_0[Prod.mk] x_5 x_4;

let x_7 : obj := ctor_0[List.nil];

let x_8 : obj := ctor_1[List.cons] x_6 x_7;

let x_9 : obj := proj[1] x_1;

inc x_9;

dec x_1;

let x_10 : obj := ctor_3[Lean.Json.str] x_9;

let x_11 : obj := _private.tests.lean.run.toFromJson.0.toJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1421._closed_2;

let x_11 : obj := _private.lean.run.toFromJson.0.toJsonFoo.«_@».lean.run.toFromJson._hyg.1421._closed_2;

let x_12 : obj := ctor_0[Prod.mk] x_11 x_10;

let x_13 : obj := ctor_1[List.cons] x_12 x_7;

let x_14 : obj := ctor_1[List.cons] x_13 x_7;

let x_15 : obj := ctor_1[List.cons] x_8 x_14;

let x_16 : obj := _aux_tests_lean_run_toFromJson___macroRules_termJson__1._closed_1;

let x_16 : obj := _aux_lean_run_toFromJson___macroRules_termJson__1._closed_1;

let x_17 : obj := List.bindTR.go._at._private.Lean.Util.Paths.0.Lean.toJsonLeanPaths.«_@».Lean.Util.Paths._hyg.40._spec_2 x_15 x_16;

let x_18 : obj := Lean.Json.mkObj x_17;

ret x_18

[result]

def instToJsonFoo._closed_1 : obj :=

let x_1 : obj := pap _private.tests.lean.run.toFromJson.0.toJsonFoo._@.tests.lean.run.toFromJson._hyg.1421;

let x_1 : obj := pap _private.lean.run.toFromJson.0.toJsonFoo._@.lean.run.toFromJson._hyg.1421;

ret x_1

def instToJsonFoo : obj :=

let x_1 : obj := instToJsonFoo._closed_1;

ret x_1

[result]

def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._lambda_1 (x_1 : @& obj) : u8 :=

def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._lambda_1 (x_1 : @& obj) : u8 :=

let x_2 : u8 := 0;

ret x_2

def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_1 : obj :=

def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_1 : obj :=

let x_1 : obj := "Foo";

ret x_1

def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_2 : obj :=

def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_2 : obj :=

let x_1 : obj := ctor_0[Lean.Name.anonymous._impl];

let x_2 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_1;

let x_2 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_1;

let x_3 : obj := Lean.Name.str._override x_1 x_2;

ret x_3

def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_3 : obj :=

def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_3 : obj :=

let x_1 : obj := pap _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._lambda_1._boxed;

let x_1 : obj := pap _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._lambda_1._boxed;

ret x_1

def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_4 : obj :=

def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_4 : obj :=

let x_1 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_2;

let x_1 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_2;

let x_2 : u8 := 1;

let x_3 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_3;

let x_3 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_3;

let x_4 : obj := Lean.Name.toString x_1 x_2 x_3;

ret x_4

def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_5 : obj :=

def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_5 : obj :=

let x_1 : obj := ".";

ret x_1

def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_6 : obj :=

def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_6 : obj :=

let x_1 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_4;

let x_1 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_4;

let x_2 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_5;

let x_2 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_5;

let x_3 : obj := String.append x_1 x_2;

dec x_2;

ret x_3

def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_7 : obj :=

def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_7 : obj :=

let x_1 : obj := ctor_0[Lean.Name.anonymous._impl];

let x_2 : obj := _private.tests.lean.run.toFromJson.0.toJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1421._closed_1;

let x_2 : obj := _private.lean.run.toFromJson.0.toJsonFoo.«_@».lean.run.toFromJson._hyg.1421._closed_1;

let x_3 : obj := Lean.Name.str._override x_1 x_2;

ret x_3

def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_8 : obj :=

def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_8 : obj :=

let x_1 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_7;

let x_1 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_7;

let x_2 : u8 := 1;

let x_3 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_3;

let x_3 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_3;

let x_4 : obj := Lean.Name.toString x_1 x_2 x_3;

ret x_4

def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_9 : obj :=

def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_9 : obj :=

let x_1 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_6;

let x_1 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_6;

let x_2 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_8;

let x_2 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_8;

let x_3 : obj := String.append x_1 x_2;

dec x_2;

ret x_3

def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_10 : obj :=

def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_10 : obj :=

let x_1 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_9;

let x_1 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_9;

let x_2 : obj := «mjson{_:_}»._closed_10;

let x_3 : obj := String.append x_1 x_2;

dec x_2;

ret x_3

def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_11 : obj :=

def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_11 : obj :=

let x_1 : obj := ctor_0[Lean.Name.anonymous._impl];

let x_2 : obj := _private.tests.lean.run.toFromJson.0.toJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1421._closed_2;

let x_2 : obj := _private.lean.run.toFromJson.0.toJsonFoo.«_@».lean.run.toFromJson._hyg.1421._closed_2;

let x_3 : obj := Lean.Name.str._override x_1 x_2;

ret x_3

def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_12 : obj :=

def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_12 : obj :=

let x_1 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_11;

let x_1 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_11;

let x_2 : u8 := 1;

let x_3 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_3;

let x_3 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_3;

let x_4 : obj := Lean.Name.toString x_1 x_2 x_3;

ret x_4

def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_13 : obj :=

def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_13 : obj :=

let x_1 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_6;

let x_1 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_6;

let x_2 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_12;

let x_2 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_12;

let x_3 : obj := String.append x_1 x_2;

dec x_2;

ret x_3

def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_14 : obj :=

def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_14 : obj :=

let x_1 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_13;

let x_1 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_13;

let x_2 : obj := «mjson{_:_}»._closed_10;

let x_3 : obj := String.append x_1 x_2;

dec x_2;

ret x_3

def _private.tests.lean.run.toFromJson.0.fromJsonFoo._@.tests.lean.run.toFromJson._hyg.1473 (x_1 : obj) : obj :=

def _private.lean.run.toFromJson.0.fromJsonFoo._@.lean.run.toFromJson._hyg.1469 (x_1 : obj) : obj :=

let x_2 : obj := _private.tests.lean.run.toFromJson.0.toJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1421._closed_1;

let x_2 : obj := _private.lean.run.toFromJson.0.toJsonFoo.«_@».lean.run.toFromJson._hyg.1421._closed_1;

inc x_1;

let x_3 : obj := Lean.Json.getObjValAs?._at._private.Lean.Data.Position.0.Lean.fromJsonPosition.«_@».Lean.Data.Position._hyg.285._spec_1 x_1 x_2;

dec x_2;

case x_3 : obj of

Except.error →

dec x_1;

let x_4 : u8 := isShared x_3;

case x_4 : u8 of

Bool.false →

let x_5 : obj := proj[0] x_3;

let x_6 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_10;

let x_6 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_10;

let x_7 : obj := String.append x_6 x_5;

dec x_5;

set x_3[0] := x_7;

ret x_3

Bool.true →

let x_8 : obj := proj[0] x_3;

inc x_8;

dec x_3;

let x_9 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_10;

let x_9 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_10;

let x_10 : obj := String.append x_9 x_8;

dec x_8;

let x_11 : obj := ctor_0[Except.error] x_10;

ret x_11

Except.ok →

let x_12 : obj := proj[0] x_3;

inc x_12;

dec x_3;

let x_13 : obj := _private.tests.lean.run.toFromJson.0.toJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1421._closed_2;

let x_13 : obj := _private.lean.run.toFromJson.0.toJsonFoo.«_@».lean.run.toFromJson._hyg.1421._closed_2;

let x_14 : obj := Lean.Json.getObjValAs?._at._private.Lean.Message.0.Lean.fromJsonBaseMessage.«_@».Lean.Message._hyg.2615._spec_1 x_1 x_13;

dec x_13;

case x_14 : obj of

Except.error →

dec x_12;

let x_15 : u8 := isShared x_14;

case x_15 : u8 of

Bool.false →

let x_16 : obj := proj[0] x_14;

let x_17 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_14;

let x_17 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_14;

let x_18 : obj := String.append x_17 x_16;

dec x_16;

set x_14[0] := x_18;

ret x_14

Bool.true →

let x_19 : obj := proj[0] x_14;

inc x_19;

dec x_14;

let x_20 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_14;

let x_20 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_14;

let x_21 : obj := String.append x_20 x_19;

dec x_19;

let x_22 : obj := ctor_0[Except.error] x_21;

ret x_22

Except.ok →

let x_23 : u8 := isShared x_14;

case x_23 : u8 of

Bool.false →

let x_24 : obj := proj[0] x_14;

let x_25 : obj := ctor_0[Foo.mk] x_12 x_24;

set x_14[0] := x_25;

ret x_14

Bool.true →

let x_26 : obj := proj[0] x_14;

inc x_26;

dec x_14;

let x_27 : obj := ctor_0[Foo.mk] x_12 x_26;

let x_28 : obj := ctor_1[Except.ok] x_27;

ret x_28

def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._lambda_1._boxed (x_1 : obj) : obj :=

def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._lambda_1._boxed (x_1 : obj) : obj :=

let x_2 : u8 := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._lambda_1 x_1;

let x_2 : u8 := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._lambda_1 x_1;

dec x_1;

let x_3 : obj := box x_2;

ret x_3

[result]

def instFromJsonFoo._closed_1 : obj :=

let x_1 : obj := pap _private.tests.lean.run.toFromJson.0.fromJsonFoo._@.tests.lean.run.toFromJson._hyg.1473;

let x_1 : obj := pap _private.lean.run.toFromJson.0.fromJsonFoo._@.lean.run.toFromJson._hyg.1469;

ret x_1

def instFromJsonFoo : obj :=

let x_1 : obj := instFromJsonFoo._closed_1;

ret x_1

[result]

def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_1 : obj :=

def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_1 : obj :=

let x_1 : obj := _private.tests.lean.run.toFromJson.0.toJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1421._closed_1;

let x_1 : obj := _private.lean.run.toFromJson.0.toJsonFoo.«_@».lean.run.toFromJson._hyg.1421._closed_1;

let x_2 : obj := ctor_3[Std.Format.text] x_1;

ret x_2

def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_2 : obj :=

def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_2 : obj :=

let x_1 : obj := ctor_0[Std.Format.nil];

let x_2 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_1;

let x_2 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_1;

let x_3 : obj := ctor_5[Std.Format.append] x_1 x_2;

ret x_3

def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_3 : obj :=

def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_3 : obj :=

let x_1 : obj := " := ";

ret x_1

def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_4 : obj :=

def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_4 : obj :=

let x_1 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_3;

let x_1 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_3;

let x_2 : obj := ctor_3[Std.Format.text] x_1;

ret x_2

def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_5 : obj :=

def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_5 : obj :=

let x_1 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_2;

let x_1 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_2;

let x_2 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_4;

let x_2 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_4;

let x_3 : obj := ctor_5[Std.Format.append] x_1 x_2;

ret x_3

def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_6 : obj :=

def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_6 : obj :=

let x_1 : obj := 5;

let x_2 : obj := Int.ofNat x_1;

ret x_2

def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_7 : obj :=

def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_7 : obj :=

let x_1 : obj := «mjson{_:_}»._closed_17;

let x_2 : obj := ctor_3[Std.Format.text] x_1;

ret x_2

def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_8 : obj :=

def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_8 : obj :=

let x_1 : obj := _private.tests.lean.run.toFromJson.0.toJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1421._closed_2;

let x_1 : obj := _private.lean.run.toFromJson.0.toJsonFoo.«_@».lean.run.toFromJson._hyg.1421._closed_2;

let x_2 : obj := ctor_3[Std.Format.text] x_1;

ret x_2

def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_9 : obj :=

def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_9 : obj :=

let x_1 : obj := "{ ";

ret x_1

def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_10 : obj :=

def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_10 : obj :=

let x_1 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_9;

let x_1 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_9;

let x_2 : obj := String.length x_1;

dec x_1;

ret x_2

def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_11 : obj :=

def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_11 : obj :=

let x_1 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_10;

let x_1 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_10;

let x_2 : obj := Int.ofNat x_1;

ret x_2

def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_12 : obj :=

def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_12 : obj :=

let x_1 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_9;

let x_1 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_9;

let x_2 : obj := ctor_3[Std.Format.text] x_1;

ret x_2

def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_13 : obj :=

def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_13 : obj :=

let x_1 : obj := " }";

ret x_1

def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_14 : obj :=

def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_14 : obj :=

let x_1 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_13;

let x_1 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_13;

let x_2 : obj := ctor_3[Std.Format.text] x_1;

ret x_2

def _private.tests.lean.run.toFromJson.0.reprFoo._@.tests.lean.run.toFromJson._hyg.1579 (x_1 : obj) (x_2 : @& obj) : obj :=

def _private.lean.run.toFromJson.0.reprFoo._@.lean.run.toFromJson._hyg.1571 (x_1 : obj) (x_2 : @& obj) : obj :=

let x_3 : obj := proj[0] x_1;

inc x_3;

let x_4 : obj := _private.Init.Data.Repr.0.Nat.reprFast x_3;

let x_5 : obj := ctor_3[Std.Format.text] x_4;

let x_6 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_6;

let x_6 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_6;

inc x_6;

let x_7 : obj := ctor_4[Std.Format.nest] x_6 x_5;

let x_8 : u8 := 0;

let x_9 : obj := ctor_6.0.1[Std.Format.group] x_7;

sset x_9[1, 0] : u8 := x_8;

let x_10 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_5;

let x_10 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_5;

let x_11 : obj := ctor_5[Std.Format.append] x_10 x_9;

let x_12 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_7;

let x_12 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_7;

let x_13 : obj := ctor_5[Std.Format.append] x_11 x_12;

let x_14 : obj := ctor_1[Std.Format.line];

let x_15 : obj := ctor_5[Std.Format.append] x_13 x_14;

let x_16 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_8;

let x_16 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_8;

let x_17 : obj := ctor_5[Std.Format.append] x_15 x_16;

let x_18 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_4;

let x_18 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_4;

let x_19 : obj := ctor_5[Std.Format.append] x_17 x_18;

let x_20 : obj := proj[1] x_1;

inc x_20;

dec x_1;

let x_21 : obj := String.quote x_20;

dec x_20;

let x_22 : obj := ctor_3[Std.Format.text] x_21;

let x_23 : obj := ctor_4[Std.Format.nest] x_6 x_22;

let x_24 : obj := ctor_6.0.1[Std.Format.group] x_23;

sset x_24[1, 0] : u8 := x_8;

let x_25 : obj := ctor_5[Std.Format.append] x_19 x_24;

let x_26 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_12;

let x_26 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_12;

let x_27 : obj := ctor_5[Std.Format.append] x_26 x_25;

let x_28 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_14;

let x_28 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_14;

let x_29 : obj := ctor_5[Std.Format.append] x_27 x_28;

let x_30 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_11;

let x_30 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_11;

let x_31 : obj := ctor_4[Std.Format.nest] x_30 x_29;

let x_32 : obj := ctor_6.0.1[Std.Format.group] x_31;

sset x_32[1, 0] : u8 := x_8;

ret x_32

def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._boxed (x_1 : obj) (x_2 : obj) : obj :=

def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._boxed (x_1 : obj) (x_2 : obj) : obj :=

let x_3 : obj := _private.tests.lean.run.toFromJson.0.reprFoo._@.tests.lean.run.toFromJson._hyg.1579 x_1 x_2;

let x_3 : obj := _private.lean.run.toFromJson.0.reprFoo._@.lean.run.toFromJson._hyg.1571 x_1 x_2;

dec x_2;

ret x_3

[result]

def instReprFoo._closed_1 : obj :=

let x_1 : obj := pap _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._boxed;

let x_1 : obj := pap _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._boxed;

ret x_1

def instReprFoo : obj :=

let x_1 : obj := instReprFoo._closed_1;

ret x_1

[result]

def _private.tests.lean.run.toFromJson.0.beqFoo._@.tests.lean.run.toFromJson._hyg.1637 (x_1 : @& obj) (x_2 : @& obj) : u8 :=

def _private.lean.run.toFromJson.0.beqFoo._@.lean.run.toFromJson._hyg.1629 (x_1 : @& obj) (x_2 : @& obj) : u8 :=

let x_3 : obj := proj[0] x_1;

let x_4 : obj := proj[1] x_1;

let x_5 : obj := proj[0] x_2;

let x_6 : obj := proj[1] x_2;

let x_7 : u8 := Nat.beq x_3 x_5;

case x_7 : u8 of

Bool.false →

let x_8 : u8 := 0;

ret x_8

Bool.true →

let x_9 : u8 := String.decEq x_4 x_6;

ret x_9

def _private.tests.lean.run.toFromJson.0.beqFoo.«_@».tests.lean.run.toFromJson._hyg.1637._boxed (x_1 : obj) (x_2 : obj) : obj :=

def _private.lean.run.toFromJson.0.beqFoo.«_@».lean.run.toFromJson._hyg.1629._boxed (x_1 : obj) (x_2 : obj) : obj :=

let x_3 : u8 := _private.tests.lean.run.toFromJson.0.beqFoo._@.tests.lean.run.toFromJson._hyg.1637 x_1 x_2;

let x_3 : u8 := _private.lean.run.toFromJson.0.beqFoo._@.lean.run.toFromJson._hyg.1629 x_1 x_2;

dec x_2;

dec x_1;

let x_4 : obj := box x_3;

ret x_4

[result]

def instBEqFoo._closed_1 : obj :=

let x_1 : obj := pap _private.tests.lean.run.toFromJson.0.beqFoo.«_@».tests.lean.run.toFromJson._hyg.1637._boxed;

let x_1 : obj := pap _private.lean.run.toFromJson.0.beqFoo.«_@».lean.run.toFromJson._hyg.1629._boxed;

ret x_1

def instBEqFoo : obj :=

let x_1 : obj := instBEqFoo._closed_1;

ret x_1

Gespeicherten Diffs

Original text

Datei öffnen

[result]
def _private.tests.lean.run.toFromJson.0.toJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1421._closed_1 : obj :=
  let x_1 : obj := "x";
  ret x_1
def _private.tests.lean.run.toFromJson.0.toJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1421._closed_2 : obj :=
  let x_1 : obj := "y";
  ret x_1
def _private.tests.lean.run.toFromJson.0.toJsonFoo._@.tests.lean.run.toFromJson._hyg.1421 (x_1 : obj) : obj :=
  let x_2 : obj := proj[0] x_1;
  inc x_2;
  let x_3 : obj := Lean.JsonNumber.fromNat x_2;
  let x_4 : obj := ctor_2[Lean.Json.num] x_3;
  let x_5 : obj := _private.tests.lean.run.toFromJson.0.toJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1421._closed_1;
  let x_6 : obj := ctor_0[Prod.mk] x_5 x_4;
  let x_7 : obj := ctor_0[List.nil];
  let x_8 : obj := ctor_1[List.cons] x_6 x_7;
  let x_9 : obj := proj[1] x_1;
  inc x_9;
  dec x_1;
  let x_10 : obj := ctor_3[Lean.Json.str] x_9;
  let x_11 : obj := _private.tests.lean.run.toFromJson.0.toJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1421._closed_2;
  let x_12 : obj := ctor_0[Prod.mk] x_11 x_10;
  let x_13 : obj := ctor_1[List.cons] x_12 x_7;
  let x_14 : obj := ctor_1[List.cons] x_13 x_7;
  let x_15 : obj := ctor_1[List.cons] x_8 x_14;
  let x_16 : obj := _aux_tests_lean_run_toFromJson___macroRules_termJson__1._closed_1;
  let x_17 : obj := List.bindTR.go._at._private.Lean.Util.Paths.0.Lean.toJsonLeanPaths.«_@».Lean.Util.Paths._hyg.40._spec_2 x_15 x_16;
  let x_18 : obj := Lean.Json.mkObj x_17;
  ret x_18
[result]
def instToJsonFoo._closed_1 : obj :=
  let x_1 : obj := pap _private.tests.lean.run.toFromJson.0.toJsonFoo._@.tests.lean.run.toFromJson._hyg.1421;
  ret x_1
def instToJsonFoo : obj :=
  let x_1 : obj := instToJsonFoo._closed_1;
  ret x_1
[result]
def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._lambda_1 (x_1 : @& obj) : u8 :=
  let x_2 : u8 := 0;
  ret x_2
def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_1 : obj :=
  let x_1 : obj := "Foo";
  ret x_1
def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_2 : obj :=
  let x_1 : obj := ctor_0[Lean.Name.anonymous._impl];
  let x_2 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_1;
  let x_3 : obj := Lean.Name.str._override x_1 x_2;
  ret x_3
def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_3 : obj :=
  let x_1 : obj := pap _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._lambda_1._boxed;
  ret x_1
def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_4 : obj :=
  let x_1 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_2;
  let x_2 : u8 := 1;
  let x_3 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_3;
  let x_4 : obj := Lean.Name.toString x_1 x_2 x_3;
  ret x_4
def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_5 : obj :=
  let x_1 : obj := ".";
  ret x_1
def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_6 : obj :=
  let x_1 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_4;
  let x_2 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_5;
  let x_3 : obj := String.append x_1 x_2;
  dec x_2;
  ret x_3
def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_7 : obj :=
  let x_1 : obj := ctor_0[Lean.Name.anonymous._impl];
  let x_2 : obj := _private.tests.lean.run.toFromJson.0.toJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1421._closed_1;
  let x_3 : obj := Lean.Name.str._override x_1 x_2;
  ret x_3
def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_8 : obj :=
  let x_1 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_7;
  let x_2 : u8 := 1;
  let x_3 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_3;
  let x_4 : obj := Lean.Name.toString x_1 x_2 x_3;
  ret x_4
def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_9 : obj :=
  let x_1 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_6;
  let x_2 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_8;
  let x_3 : obj := String.append x_1 x_2;
  dec x_2;
  ret x_3
def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_10 : obj :=
  let x_1 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_9;
  let x_2 : obj := «mjson{_:_}»._closed_10;
  let x_3 : obj := String.append x_1 x_2;
  dec x_2;
  ret x_3
def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_11 : obj :=
  let x_1 : obj := ctor_0[Lean.Name.anonymous._impl];
  let x_2 : obj := _private.tests.lean.run.toFromJson.0.toJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1421._closed_2;
  let x_3 : obj := Lean.Name.str._override x_1 x_2;
  ret x_3
def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_12 : obj :=
  let x_1 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_11;
  let x_2 : u8 := 1;
  let x_3 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_3;
  let x_4 : obj := Lean.Name.toString x_1 x_2 x_3;
  ret x_4
def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_13 : obj :=
  let x_1 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_6;
  let x_2 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_12;
  let x_3 : obj := String.append x_1 x_2;
  dec x_2;
  ret x_3
def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_14 : obj :=
  let x_1 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_13;
  let x_2 : obj := «mjson{_:_}»._closed_10;
  let x_3 : obj := String.append x_1 x_2;
  dec x_2;
  ret x_3
def _private.tests.lean.run.toFromJson.0.fromJsonFoo._@.tests.lean.run.toFromJson._hyg.1473 (x_1 : obj) : obj :=
  let x_2 : obj := _private.tests.lean.run.toFromJson.0.toJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1421._closed_1;
  inc x_1;
  let x_3 : obj := Lean.Json.getObjValAs?._at._private.Lean.Data.Position.0.Lean.fromJsonPosition.«_@».Lean.Data.Position._hyg.285._spec_1 x_1 x_2;
  dec x_2;
  case x_3 : obj of
  Except.error →
    dec x_1;
    let x_4 : u8 := isShared x_3;
    case x_4 : u8 of
    Bool.false →
      let x_5 : obj := proj[0] x_3;
      let x_6 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_10;
      let x_7 : obj := String.append x_6 x_5;
      dec x_5;
      set x_3[0] := x_7;
      ret x_3
    Bool.true →
      let x_8 : obj := proj[0] x_3;
      inc x_8;
      dec x_3;
      let x_9 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_10;
      let x_10 : obj := String.append x_9 x_8;
      dec x_8;
      let x_11 : obj := ctor_0[Except.error] x_10;
      ret x_11
  Except.ok →
    let x_12 : obj := proj[0] x_3;
    inc x_12;
    dec x_3;
    let x_13 : obj := _private.tests.lean.run.toFromJson.0.toJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1421._closed_2;
    let x_14 : obj := Lean.Json.getObjValAs?._at._private.Lean.Message.0.Lean.fromJsonBaseMessage.«_@».Lean.Message._hyg.2615._spec_1 x_1 x_13;
    dec x_13;
    case x_14 : obj of
    Except.error →
      dec x_12;
      let x_15 : u8 := isShared x_14;
      case x_15 : u8 of
      Bool.false →
        let x_16 : obj := proj[0] x_14;
        let x_17 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_14;
        let x_18 : obj := String.append x_17 x_16;
        dec x_16;
        set x_14[0] := x_18;
        ret x_14
      Bool.true →
        let x_19 : obj := proj[0] x_14;
        inc x_19;
        dec x_14;
        let x_20 : obj := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._closed_14;
        let x_21 : obj := String.append x_20 x_19;
        dec x_19;
        let x_22 : obj := ctor_0[Except.error] x_21;
        ret x_22
    Except.ok →
      let x_23 : u8 := isShared x_14;
      case x_23 : u8 of
      Bool.false →
        let x_24 : obj := proj[0] x_14;
        let x_25 : obj := ctor_0[Foo.mk] x_12 x_24;
        set x_14[0] := x_25;
        ret x_14
      Bool.true →
        let x_26 : obj := proj[0] x_14;
        inc x_26;
        dec x_14;
        let x_27 : obj := ctor_0[Foo.mk] x_12 x_26;
        let x_28 : obj := ctor_1[Except.ok] x_27;
        ret x_28
def _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._lambda_1._boxed (x_1 : obj) : obj :=
  let x_2 : u8 := _private.tests.lean.run.toFromJson.0.fromJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1473._lambda_1 x_1;
  dec x_1;
  let x_3 : obj := box x_2;
  ret x_3
[result]
def instFromJsonFoo._closed_1 : obj :=
  let x_1 : obj := pap _private.tests.lean.run.toFromJson.0.fromJsonFoo._@.tests.lean.run.toFromJson._hyg.1473;
  ret x_1
def instFromJsonFoo : obj :=
  let x_1 : obj := instFromJsonFoo._closed_1;
  ret x_1
[result]
def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_1 : obj :=
  let x_1 : obj := _private.tests.lean.run.toFromJson.0.toJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1421._closed_1;
  let x_2 : obj := ctor_3[Std.Format.text] x_1;
  ret x_2
def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_2 : obj :=
  let x_1 : obj := ctor_0[Std.Format.nil];
  let x_2 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_1;
  let x_3 : obj := ctor_5[Std.Format.append] x_1 x_2;
  ret x_3
def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_3 : obj :=
  let x_1 : obj := " := ";
  ret x_1
def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_4 : obj :=
  let x_1 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_3;
  let x_2 : obj := ctor_3[Std.Format.text] x_1;
  ret x_2
def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_5 : obj :=
  let x_1 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_2;
  let x_2 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_4;
  let x_3 : obj := ctor_5[Std.Format.append] x_1 x_2;
  ret x_3
def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_6 : obj :=
  let x_1 : obj := 5;
  let x_2 : obj := Int.ofNat x_1;
  ret x_2
def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_7 : obj :=
  let x_1 : obj := «mjson{_:_}»._closed_17;
  let x_2 : obj := ctor_3[Std.Format.text] x_1;
  ret x_2
def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_8 : obj :=
  let x_1 : obj := _private.tests.lean.run.toFromJson.0.toJsonFoo.«_@».tests.lean.run.toFromJson._hyg.1421._closed_2;
  let x_2 : obj := ctor_3[Std.Format.text] x_1;
  ret x_2
def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_9 : obj :=
  let x_1 : obj := "{ ";
  ret x_1
def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_10 : obj :=
  let x_1 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_9;
  let x_2 : obj := String.length x_1;
  dec x_1;
  ret x_2
def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_11 : obj :=
  let x_1 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_10;
  let x_2 : obj := Int.ofNat x_1;
  ret x_2
def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_12 : obj :=
  let x_1 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_9;
  let x_2 : obj := ctor_3[Std.Format.text] x_1;
  ret x_2
def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_13 : obj :=
  let x_1 : obj := " }";
  ret x_1
def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_14 : obj :=
  let x_1 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_13;
  let x_2 : obj := ctor_3[Std.Format.text] x_1;
  ret x_2
def _private.tests.lean.run.toFromJson.0.reprFoo._@.tests.lean.run.toFromJson._hyg.1579 (x_1 : obj) (x_2 : @& obj) : obj :=
  let x_3 : obj := proj[0] x_1;
  inc x_3;
  let x_4 : obj := _private.Init.Data.Repr.0.Nat.reprFast x_3;
  let x_5 : obj := ctor_3[Std.Format.text] x_4;
  let x_6 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_6;
  inc x_6;
  let x_7 : obj := ctor_4[Std.Format.nest] x_6 x_5;
  let x_8 : u8 := 0;
  let x_9 : obj := ctor_6.0.1[Std.Format.group] x_7;
  sset x_9[1, 0] : u8 := x_8;
  let x_10 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_5;
  let x_11 : obj := ctor_5[Std.Format.append] x_10 x_9;
  let x_12 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_7;
  let x_13 : obj := ctor_5[Std.Format.append] x_11 x_12;
  let x_14 : obj := ctor_1[Std.Format.line];
  let x_15 : obj := ctor_5[Std.Format.append] x_13 x_14;
  let x_16 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_8;
  let x_17 : obj := ctor_5[Std.Format.append] x_15 x_16;
  let x_18 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_4;
  let x_19 : obj := ctor_5[Std.Format.append] x_17 x_18;
  let x_20 : obj := proj[1] x_1;
  inc x_20;
  dec x_1;
  let x_21 : obj := String.quote x_20;
  dec x_20;
  let x_22 : obj := ctor_3[Std.Format.text] x_21;
  let x_23 : obj := ctor_4[Std.Format.nest] x_6 x_22;
  let x_24 : obj := ctor_6.0.1[Std.Format.group] x_23;
  sset x_24[1, 0] : u8 := x_8;
  let x_25 : obj := ctor_5[Std.Format.append] x_19 x_24;
  let x_26 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_12;
  let x_27 : obj := ctor_5[Std.Format.append] x_26 x_25;
  let x_28 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_14;
  let x_29 : obj := ctor_5[Std.Format.append] x_27 x_28;
  let x_30 : obj := _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._closed_11;
  let x_31 : obj := ctor_4[Std.Format.nest] x_30 x_29;
  let x_32 : obj := ctor_6.0.1[Std.Format.group] x_31;
  sset x_32[1, 0] : u8 := x_8;
  ret x_32
def _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._boxed (x_1 : obj) (x_2 : obj) : obj :=
  let x_3 : obj := _private.tests.lean.run.toFromJson.0.reprFoo._@.tests.lean.run.toFromJson._hyg.1579 x_1 x_2;
  dec x_2;
  ret x_3
[result]
def instReprFoo._closed_1 : obj :=
  let x_1 : obj := pap _private.tests.lean.run.toFromJson.0.reprFoo.«_@».tests.lean.run.toFromJson._hyg.1579._boxed;
  ret x_1
def instReprFoo : obj :=
  let x_1 : obj := instReprFoo._closed_1;
  ret x_1
[result]
def _private.tests.lean.run.toFromJson.0.beqFoo._@.tests.lean.run.toFromJson._hyg.1637 (x_1 : @& obj) (x_2 : @& obj) : u8 :=
  let x_3 : obj := proj[0] x_1;
  let x_4 : obj := proj[1] x_1;
  let x_5 : obj := proj[0] x_2;
  let x_6 : obj := proj[1] x_2;
  let x_7 : u8 := Nat.beq x_3 x_5;
  case x_7 : u8 of
  Bool.false →
    let x_8 : u8 := 0;
    ret x_8
  Bool.true →
    let x_9 : u8 := String.decEq x_4 x_6;
    ret x_9
def _private.tests.lean.run.toFromJson.0.beqFoo.«_@».tests.lean.run.toFromJson._hyg.1637._boxed (x_1 : obj) (x_2 : obj) : obj :=
  let x_3 : u8 := _private.tests.lean.run.toFromJson.0.beqFoo._@.tests.lean.run.toFromJson._hyg.1637 x_1 x_2;
  dec x_2;
  dec x_1;
  let x_4 : obj := box x_3;
  ret x_4
[result]
def instBEqFoo._closed_1 : obj :=
  let x_1 : obj := pap _private.tests.lean.run.toFromJson.0.beqFoo.«_@».tests.lean.run.toFromJson._hyg.1637._boxed;
  ret x_1
def instBEqFoo : obj :=
  let x_1 : obj := instBEqFoo._closed_1;
  ret x_1

Geänderter text

Datei öffnen

[result]
def _private.lean.run.toFromJson.0.toJsonFoo.«_@».lean.run.toFromJson._hyg.1421._closed_1 : obj :=
  let x_1 : obj := "x";
  ret x_1
def _private.lean.run.toFromJson.0.toJsonFoo.«_@».lean.run.toFromJson._hyg.1421._closed_2 : obj :=
  let x_1 : obj := "y";
  ret x_1
def _private.lean.run.toFromJson.0.toJsonFoo._@.lean.run.toFromJson._hyg.1421 (x_1 : obj) : obj :=
  let x_2 : obj := proj[0] x_1;
  inc x_2;
  let x_3 : obj := Lean.JsonNumber.fromNat x_2;
  let x_4 : obj := ctor_2[Lean.Json.num] x_3;
  let x_5 : obj := _private.lean.run.toFromJson.0.toJsonFoo.«_@».lean.run.toFromJson._hyg.1421._closed_1;
  let x_6 : obj := ctor_0[Prod.mk] x_5 x_4;
  let x_7 : obj := ctor_0[List.nil];
  let x_8 : obj := ctor_1[List.cons] x_6 x_7;
  let x_9 : obj := proj[1] x_1;
  inc x_9;
  dec x_1;
  let x_10 : obj := ctor_3[Lean.Json.str] x_9;
  let x_11 : obj := _private.lean.run.toFromJson.0.toJsonFoo.«_@».lean.run.toFromJson._hyg.1421._closed_2;
  let x_12 : obj := ctor_0[Prod.mk] x_11 x_10;
  let x_13 : obj := ctor_1[List.cons] x_12 x_7;
  let x_14 : obj := ctor_1[List.cons] x_13 x_7;
  let x_15 : obj := ctor_1[List.cons] x_8 x_14;
  let x_16 : obj := _aux_lean_run_toFromJson___macroRules_termJson__1._closed_1;
  let x_17 : obj := List.bindTR.go._at._private.Lean.Util.Paths.0.Lean.toJsonLeanPaths.«_@».Lean.Util.Paths._hyg.40._spec_2 x_15 x_16;
  let x_18 : obj := Lean.Json.mkObj x_17;
  ret x_18
[result]
def instToJsonFoo._closed_1 : obj :=
  let x_1 : obj := pap _private.lean.run.toFromJson.0.toJsonFoo._@.lean.run.toFromJson._hyg.1421;
  ret x_1
def instToJsonFoo : obj :=
  let x_1 : obj := instToJsonFoo._closed_1;
  ret x_1
[result]
def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._lambda_1 (x_1 : @& obj) : u8 :=
  let x_2 : u8 := 0;
  ret x_2
def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_1 : obj :=
  let x_1 : obj := "Foo";
  ret x_1
def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_2 : obj :=
  let x_1 : obj := ctor_0[Lean.Name.anonymous._impl];
  let x_2 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_1;
  let x_3 : obj := Lean.Name.str._override x_1 x_2;
  ret x_3
def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_3 : obj :=
  let x_1 : obj := pap _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._lambda_1._boxed;
  ret x_1
def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_4 : obj :=
  let x_1 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_2;
  let x_2 : u8 := 1;
  let x_3 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_3;
  let x_4 : obj := Lean.Name.toString x_1 x_2 x_3;
  ret x_4
def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_5 : obj :=
  let x_1 : obj := ".";
  ret x_1
def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_6 : obj :=
  let x_1 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_4;
  let x_2 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_5;
  let x_3 : obj := String.append x_1 x_2;
  dec x_2;
  ret x_3
def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_7 : obj :=
  let x_1 : obj := ctor_0[Lean.Name.anonymous._impl];
  let x_2 : obj := _private.lean.run.toFromJson.0.toJsonFoo.«_@».lean.run.toFromJson._hyg.1421._closed_1;
  let x_3 : obj := Lean.Name.str._override x_1 x_2;
  ret x_3
def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_8 : obj :=
  let x_1 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_7;
  let x_2 : u8 := 1;
  let x_3 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_3;
  let x_4 : obj := Lean.Name.toString x_1 x_2 x_3;
  ret x_4
def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_9 : obj :=
  let x_1 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_6;
  let x_2 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_8;
  let x_3 : obj := String.append x_1 x_2;
  dec x_2;
  ret x_3
def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_10 : obj :=
  let x_1 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_9;
  let x_2 : obj := «mjson{_:_}»._closed_10;
  let x_3 : obj := String.append x_1 x_2;
  dec x_2;
  ret x_3
def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_11 : obj :=
  let x_1 : obj := ctor_0[Lean.Name.anonymous._impl];
  let x_2 : obj := _private.lean.run.toFromJson.0.toJsonFoo.«_@».lean.run.toFromJson._hyg.1421._closed_2;
  let x_3 : obj := Lean.Name.str._override x_1 x_2;
  ret x_3
def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_12 : obj :=
  let x_1 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_11;
  let x_2 : u8 := 1;
  let x_3 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_3;
  let x_4 : obj := Lean.Name.toString x_1 x_2 x_3;
  ret x_4
def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_13 : obj :=
  let x_1 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_6;
  let x_2 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_12;
  let x_3 : obj := String.append x_1 x_2;
  dec x_2;
  ret x_3
def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_14 : obj :=
  let x_1 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_13;
  let x_2 : obj := «mjson{_:_}»._closed_10;
  let x_3 : obj := String.append x_1 x_2;
  dec x_2;
  ret x_3
def _private.lean.run.toFromJson.0.fromJsonFoo._@.lean.run.toFromJson._hyg.1469 (x_1 : obj) : obj :=
  let x_2 : obj := _private.lean.run.toFromJson.0.toJsonFoo.«_@».lean.run.toFromJson._hyg.1421._closed_1;
  inc x_1;
  let x_3 : obj := Lean.Json.getObjValAs?._at._private.Lean.Data.Position.0.Lean.fromJsonPosition.«_@».Lean.Data.Position._hyg.285._spec_1 x_1 x_2;
  dec x_2;
  case x_3 : obj of
  Except.error →
    dec x_1;
    let x_4 : u8 := isShared x_3;
    case x_4 : u8 of
    Bool.false →
      let x_5 : obj := proj[0] x_3;
      let x_6 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_10;
      let x_7 : obj := String.append x_6 x_5;
      dec x_5;
      set x_3[0] := x_7;
      ret x_3
    Bool.true →
      let x_8 : obj := proj[0] x_3;
      inc x_8;
      dec x_3;
      let x_9 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_10;
      let x_10 : obj := String.append x_9 x_8;
      dec x_8;
      let x_11 : obj := ctor_0[Except.error] x_10;
      ret x_11
  Except.ok →
    let x_12 : obj := proj[0] x_3;
    inc x_12;
    dec x_3;
    let x_13 : obj := _private.lean.run.toFromJson.0.toJsonFoo.«_@».lean.run.toFromJson._hyg.1421._closed_2;
    let x_14 : obj := Lean.Json.getObjValAs?._at._private.Lean.Message.0.Lean.fromJsonBaseMessage.«_@».Lean.Message._hyg.2615._spec_1 x_1 x_13;
    dec x_13;
    case x_14 : obj of
    Except.error →
      dec x_12;
      let x_15 : u8 := isShared x_14;
      case x_15 : u8 of
      Bool.false →
        let x_16 : obj := proj[0] x_14;
        let x_17 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_14;
        let x_18 : obj := String.append x_17 x_16;
        dec x_16;
        set x_14[0] := x_18;
        ret x_14
      Bool.true →
        let x_19 : obj := proj[0] x_14;
        inc x_19;
        dec x_14;
        let x_20 : obj := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._closed_14;
        let x_21 : obj := String.append x_20 x_19;
        dec x_19;
        let x_22 : obj := ctor_0[Except.error] x_21;
        ret x_22
    Except.ok →
      let x_23 : u8 := isShared x_14;
      case x_23 : u8 of
      Bool.false →
        let x_24 : obj := proj[0] x_14;
        let x_25 : obj := ctor_0[Foo.mk] x_12 x_24;
        set x_14[0] := x_25;
        ret x_14
      Bool.true →
        let x_26 : obj := proj[0] x_14;
        inc x_26;
        dec x_14;
        let x_27 : obj := ctor_0[Foo.mk] x_12 x_26;
        let x_28 : obj := ctor_1[Except.ok] x_27;
        ret x_28
def _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._lambda_1._boxed (x_1 : obj) : obj :=
  let x_2 : u8 := _private.lean.run.toFromJson.0.fromJsonFoo.«_@».lean.run.toFromJson._hyg.1469._lambda_1 x_1;
  dec x_1;
  let x_3 : obj := box x_2;
  ret x_3
[result]
def instFromJsonFoo._closed_1 : obj :=
  let x_1 : obj := pap _private.lean.run.toFromJson.0.fromJsonFoo._@.lean.run.toFromJson._hyg.1469;
  ret x_1
def instFromJsonFoo : obj :=
  let x_1 : obj := instFromJsonFoo._closed_1;
  ret x_1
[result]
def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_1 : obj :=
  let x_1 : obj := _private.lean.run.toFromJson.0.toJsonFoo.«_@».lean.run.toFromJson._hyg.1421._closed_1;
  let x_2 : obj := ctor_3[Std.Format.text] x_1;
  ret x_2
def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_2 : obj :=
  let x_1 : obj := ctor_0[Std.Format.nil];
  let x_2 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_1;
  let x_3 : obj := ctor_5[Std.Format.append] x_1 x_2;
  ret x_3
def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_3 : obj :=
  let x_1 : obj := " := ";
  ret x_1
def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_4 : obj :=
  let x_1 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_3;
  let x_2 : obj := ctor_3[Std.Format.text] x_1;
  ret x_2
def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_5 : obj :=
  let x_1 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_2;
  let x_2 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_4;
  let x_3 : obj := ctor_5[Std.Format.append] x_1 x_2;
  ret x_3
def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_6 : obj :=
  let x_1 : obj := 5;
  let x_2 : obj := Int.ofNat x_1;
  ret x_2
def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_7 : obj :=
  let x_1 : obj := «mjson{_:_}»._closed_17;
  let x_2 : obj := ctor_3[Std.Format.text] x_1;
  ret x_2
def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_8 : obj :=
  let x_1 : obj := _private.lean.run.toFromJson.0.toJsonFoo.«_@».lean.run.toFromJson._hyg.1421._closed_2;
  let x_2 : obj := ctor_3[Std.Format.text] x_1;
  ret x_2
def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_9 : obj :=
  let x_1 : obj := "{ ";
  ret x_1
def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_10 : obj :=
  let x_1 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_9;
  let x_2 : obj := String.length x_1;
  dec x_1;
  ret x_2
def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_11 : obj :=
  let x_1 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_10;
  let x_2 : obj := Int.ofNat x_1;
  ret x_2
def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_12 : obj :=
  let x_1 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_9;
  let x_2 : obj := ctor_3[Std.Format.text] x_1;
  ret x_2
def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_13 : obj :=
  let x_1 : obj := " }";
  ret x_1
def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_14 : obj :=
  let x_1 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_13;
  let x_2 : obj := ctor_3[Std.Format.text] x_1;
  ret x_2
def _private.lean.run.toFromJson.0.reprFoo._@.lean.run.toFromJson._hyg.1571 (x_1 : obj) (x_2 : @& obj) : obj :=
  let x_3 : obj := proj[0] x_1;
  inc x_3;
  let x_4 : obj := _private.Init.Data.Repr.0.Nat.reprFast x_3;
  let x_5 : obj := ctor_3[Std.Format.text] x_4;
  let x_6 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_6;
  inc x_6;
  let x_7 : obj := ctor_4[Std.Format.nest] x_6 x_5;
  let x_8 : u8 := 0;
  let x_9 : obj := ctor_6.0.1[Std.Format.group] x_7;
  sset x_9[1, 0] : u8 := x_8;
  let x_10 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_5;
  let x_11 : obj := ctor_5[Std.Format.append] x_10 x_9;
  let x_12 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_7;
  let x_13 : obj := ctor_5[Std.Format.append] x_11 x_12;
  let x_14 : obj := ctor_1[Std.Format.line];
  let x_15 : obj := ctor_5[Std.Format.append] x_13 x_14;
  let x_16 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_8;
  let x_17 : obj := ctor_5[Std.Format.append] x_15 x_16;
  let x_18 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_4;
  let x_19 : obj := ctor_5[Std.Format.append] x_17 x_18;
  let x_20 : obj := proj[1] x_1;
  inc x_20;
  dec x_1;
  let x_21 : obj := String.quote x_20;
  dec x_20;
  let x_22 : obj := ctor_3[Std.Format.text] x_21;
  let x_23 : obj := ctor_4[Std.Format.nest] x_6 x_22;
  let x_24 : obj := ctor_6.0.1[Std.Format.group] x_23;
  sset x_24[1, 0] : u8 := x_8;
  let x_25 : obj := ctor_5[Std.Format.append] x_19 x_24;
  let x_26 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_12;
  let x_27 : obj := ctor_5[Std.Format.append] x_26 x_25;
  let x_28 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_14;
  let x_29 : obj := ctor_5[Std.Format.append] x_27 x_28;
  let x_30 : obj := _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._closed_11;
  let x_31 : obj := ctor_4[Std.Format.nest] x_30 x_29;
  let x_32 : obj := ctor_6.0.1[Std.Format.group] x_31;
  sset x_32[1, 0] : u8 := x_8;
  ret x_32
def _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._boxed (x_1 : obj) (x_2 : obj) : obj :=
  let x_3 : obj := _private.lean.run.toFromJson.0.reprFoo._@.lean.run.toFromJson._hyg.1571 x_1 x_2;
  dec x_2;
  ret x_3
[result]
def instReprFoo._closed_1 : obj :=
  let x_1 : obj := pap _private.lean.run.toFromJson.0.reprFoo.«_@».lean.run.toFromJson._hyg.1571._boxed;
  ret x_1
def instReprFoo : obj :=
  let x_1 : obj := instReprFoo._closed_1;
  ret x_1
[result]
def _private.lean.run.toFromJson.0.beqFoo._@.lean.run.toFromJson._hyg.1629 (x_1 : @& obj) (x_2 : @& obj) : u8 :=
  let x_3 : obj := proj[0] x_1;
  let x_4 : obj := proj[1] x_1;
  let x_5 : obj := proj[0] x_2;
  let x_6 : obj := proj[1] x_2;
  let x_7 : u8 := Nat.beq x_3 x_5;
  case x_7 : u8 of
  Bool.false →
    let x_8 : u8 := 0;
    ret x_8
  Bool.true →
    let x_9 : u8 := String.decEq x_4 x_6;
    ret x_9
def _private.lean.run.toFromJson.0.beqFoo.«_@».lean.run.toFromJson._hyg.1629._boxed (x_1 : obj) (x_2 : obj) : obj :=
  let x_3 : u8 := _private.lean.run.toFromJson.0.beqFoo._@.lean.run.toFromJson._hyg.1629 x_1 x_2;
  dec x_2;
  dec x_1;
  let x_4 : obj := box x_3;
  ret x_4
[result]
def instBEqFoo._closed_1 : obj :=
  let x_1 : obj := pap _private.lean.run.toFromJson.0.beqFoo.«_@».lean.run.toFromJson._hyg.1629._boxed;
  ret x_1
def instBEqFoo : obj :=
  let x_1 : obj := instBEqFoo._closed_1;
  ret x_1

Words removed	90
Total words	1659
Words removed (%)	5.42

Words added	90
Total words	1659
Words added (%)	5.42