306 lines
5.1 KiB
Text
306 lines
5.1 KiB
Text
structure Foo where
|
|
x1 : Nat := 0
|
|
x2 : Nat := 0
|
|
x3 : Nat := 0
|
|
x4 : Nat := 0
|
|
x5 : Nat := 0
|
|
x6 : Nat := 0
|
|
x7 : Nat := 0
|
|
x8 : Nat := 0
|
|
x9 : Nat := 0
|
|
x10 : Nat := 0
|
|
x11 : Nat := 0
|
|
x12 : Nat := 0
|
|
x13 : Nat := 0
|
|
x14 : Nat := 0
|
|
x15 : Nat := 0
|
|
x16 : Nat := 0
|
|
x17 : Nat := 0
|
|
x18 : Nat := 0
|
|
x19 : Nat := 0
|
|
x20 : Nat := 0
|
|
x21 : Nat := 0
|
|
x22 : Nat := 0
|
|
x23 : Nat := 0
|
|
x24 : Nat := 0
|
|
x25 : Nat := 0
|
|
x26 : Nat := 0
|
|
x27 : Nat := 0
|
|
x28 : Nat := 0
|
|
x29 : Nat := 0
|
|
x30 : Nat := 0
|
|
x31 : Nat := 0
|
|
x32 : Nat := 0
|
|
x33 : Nat := 0
|
|
x34 : Nat := 0
|
|
x35 : Nat := 0
|
|
x36 : Nat := 0
|
|
x37 : Nat := 0
|
|
x38 : Nat := 0
|
|
x39 : Nat := 0
|
|
x40 : Nat := 0
|
|
x41 : Nat := 0
|
|
x42 : Nat := 0
|
|
x43 : Nat := 0
|
|
x44 : Nat := 0
|
|
x45 : Nat := 0
|
|
x46 : Nat := 0
|
|
x47 : Nat := 0
|
|
x48 : Nat := 0
|
|
x49 : Nat := 0
|
|
x50 : Nat := 0
|
|
x51 : Nat := 0
|
|
x52 : Nat := 0
|
|
x53 : Nat := 0
|
|
x54 : Nat := 0
|
|
x55 : Nat := 0
|
|
x56 : Nat := 0
|
|
x57 : Nat := 0
|
|
x58 : Nat := 0
|
|
x59 : Nat := 0
|
|
x60 : Nat := 0
|
|
y1 : Nat := 0
|
|
y2 : Nat := 0
|
|
y3 : Nat := 0
|
|
y4 : Nat := 0
|
|
y5 : Nat := 0
|
|
y6 : Nat := 0
|
|
y7 : Nat := 0
|
|
y8 : Nat := 0
|
|
y9 : Nat := 0
|
|
y10 : Nat := 0
|
|
y11 : Nat := 0
|
|
y12 : Nat := 0
|
|
y13 : Nat := 0
|
|
y14 : Nat := 0
|
|
y15 : Nat := 0
|
|
y16 : Nat := 0
|
|
y17 : Nat := 0
|
|
y18 : Nat := 0
|
|
y19 : Nat := 0
|
|
y20 : Nat := 0
|
|
y21 : Nat := 0
|
|
y22 : Nat := 0
|
|
y23 : Nat := 0
|
|
y24 : Nat := 0
|
|
y25 : Nat := 0
|
|
y26 : Nat := 0
|
|
y27 : Nat := 0
|
|
y28 : Nat := 0
|
|
y29 : Nat := 0
|
|
y30 : Nat := 0
|
|
y31 : Nat := 0
|
|
y32 : Nat := 0
|
|
y33 : Nat := 0
|
|
y34 : Nat := 0
|
|
y35 : Nat := 0
|
|
y36 : Nat := 0
|
|
y37 : Nat := 0
|
|
y38 : Nat := 0
|
|
y39 : Nat := 0
|
|
y40 : Nat := 0
|
|
y41 : Nat := 0
|
|
y42 : Nat := 0
|
|
y43 : Nat := 0
|
|
y44 : Nat := 0
|
|
y45 : Nat := 0
|
|
y46 : Nat := 0
|
|
y47 : Nat := 0
|
|
y48 : Nat := 0
|
|
y49 : Nat := 0
|
|
y50 : Nat := 0
|
|
y51 : Nat := 0
|
|
y52 : Nat := 0
|
|
y53 : Nat := 0
|
|
y54 : Nat := 0
|
|
y55 : Nat := 0
|
|
y56 : Nat := 0
|
|
y57 : Nat := 0
|
|
y58 : Nat := 0
|
|
y59 : Nat := 0
|
|
y60 : Nat := 0
|
|
z1 : Nat := 0
|
|
z2 : Nat := 0
|
|
z3 : Nat := 0
|
|
z4 : Nat := 0
|
|
z5 : Nat := 0
|
|
z6 : Nat := 0
|
|
z7 : Nat := 0
|
|
z8 : Nat := 0
|
|
z9 : Nat := 0
|
|
z10 : Nat := 0
|
|
z11 : Nat := 0
|
|
z12 : Nat := 0
|
|
z13 : Nat := 0
|
|
z14 : Nat := 0
|
|
z15 : Nat := 0
|
|
z16 : Nat := 0
|
|
z17 : Nat := 0
|
|
z18 : Nat := 0
|
|
z19 : Nat := 0
|
|
z20 : Nat := 0
|
|
z21 : Nat := 0
|
|
z22 : Nat := 0
|
|
z23 : Nat := 0
|
|
z24 : Nat := 0
|
|
z25 : Nat := 0
|
|
z26 : Nat := 0
|
|
z27 : Nat := 0
|
|
z28 : Nat := 0
|
|
z29 : Nat := 0
|
|
z30 : Nat := 0
|
|
z31 : Nat := 0
|
|
z32 : Nat := 0
|
|
z33 : Nat := 0
|
|
z34 : Nat := 0
|
|
z35 : Nat := 0
|
|
z36 : Nat := 0
|
|
z37 : Nat := 0
|
|
z38 : Nat := 0
|
|
z39 : Nat := 0
|
|
z40 : Nat := 0
|
|
z41 : Nat := 0
|
|
z42 : Nat := 0
|
|
z43 : Nat := 0
|
|
z44 : Nat := 0
|
|
z45 : Nat := 0
|
|
z46 : Nat := 0
|
|
z47 : Nat := 0
|
|
z48 : Nat := 0
|
|
z49 : Nat := 0
|
|
z50 : Nat := 0
|
|
z51 : Nat := 0
|
|
z52 : Nat := 0
|
|
z53 : Nat := 0
|
|
z54 : Nat := 0
|
|
z55 : Nat := 0
|
|
z56 : Nat := 0
|
|
z57 : Nat := 0
|
|
z58 : Nat := 0
|
|
z59 : Nat := 0
|
|
z60 : Nat := 0
|
|
w1 : Nat := 0
|
|
w2 : Nat := 0
|
|
w3 : Nat := 0
|
|
w4 : Nat := 0
|
|
w5 : Nat := 0
|
|
w6 : Nat := 0
|
|
w7 : Nat := 0
|
|
w8 : Nat := 0
|
|
w9 : Nat := 0
|
|
w10 : Nat := 0
|
|
w11 : Nat := 0
|
|
w12 : Nat := 0
|
|
w13 : Nat := 0
|
|
w14 : Nat := 0
|
|
w15 : Nat := 0
|
|
w16 : Nat := 0
|
|
w17 : Nat := 0
|
|
w18 : Nat := 0
|
|
w19 : Nat := 0
|
|
w20 : Nat := 0
|
|
w21 : Nat := 0
|
|
w22 : Nat := 0
|
|
w23 : Nat := 0
|
|
w24 : Nat := 0
|
|
w25 : Nat := 0
|
|
w26 : Nat := 0
|
|
w27 : Nat := 0
|
|
w28 : Nat := 0
|
|
w29 : Nat := 0
|
|
w30 : Nat := 0
|
|
w31 : Nat := 0
|
|
w32 : Nat := 0
|
|
w33 : Nat := 0
|
|
w34 : Nat := 0
|
|
w35 : Nat := 0
|
|
w36 : Nat := 0
|
|
w37 : Nat := 0
|
|
w38 : Nat := 0
|
|
w39 : Nat := 0
|
|
w40 : Nat := 0
|
|
w41 : Nat := 0
|
|
w42 : Nat := 0
|
|
w43 : Nat := 0
|
|
w44 : Nat := 0
|
|
w45 : Nat := 0
|
|
w46 : Nat := 0
|
|
w47 : Nat := 0
|
|
w48 : Nat := 0
|
|
w49 : Nat := 0
|
|
w50 : Nat := 0
|
|
w51 : Nat := 0
|
|
w52 : Nat := 0
|
|
w53 : Nat := 0
|
|
w54 : Nat := 0
|
|
w55 : Nat := 0
|
|
w56 : Nat := 0
|
|
w57 : Nat := 0
|
|
w58 : Nat := 0
|
|
w59 : Nat := 0
|
|
w60 : Nat := 0
|
|
xx1 : Nat := 0
|
|
xx2 : Nat := 0
|
|
xx3 : Nat := 0
|
|
xx4 : Nat := 0
|
|
xx5 : Nat := 0
|
|
xx6 : Nat := 0
|
|
xx7 : Nat := 0
|
|
xx8 : Nat := 0
|
|
xx9 : Nat := 0
|
|
xx10 : Nat := 0
|
|
xx11 : Nat := 0
|
|
xx12 : Nat := 0
|
|
xx13 : Nat := 0
|
|
xx14 : Nat := 0
|
|
xx15 : Nat := 0
|
|
xx16 : Nat := 0
|
|
xx17 : Nat := 0
|
|
xx18 : Nat := 0
|
|
xx19 : Nat := 0
|
|
xx20 : Nat := 0
|
|
xx21 : Nat := 0
|
|
xx22 : Nat := 0
|
|
xx23 : Nat := 0
|
|
xx24 : Nat := 0
|
|
xx25 : Nat := 0
|
|
xx26 : Nat := 0
|
|
xx27 : Nat := 0
|
|
xx28 : Nat := 0
|
|
xx29 : Nat := 0
|
|
xx30 : Nat := 0
|
|
xx31 : Nat := 0
|
|
xx32 : Nat := 0
|
|
xx33 : Nat := 0
|
|
xx34 : Nat := 0
|
|
xx35 : Nat := 0
|
|
xx36 : Nat := 0
|
|
xx37 : Nat := 0
|
|
xx38 : Nat := 0
|
|
xx39 : Nat := 0
|
|
xx40 : Nat := 0
|
|
xx41 : Nat := 0
|
|
xx42 : Nat := 0
|
|
xx43 : Nat := 0
|
|
xx44 : Nat := 0
|
|
xx45 : Nat := 0
|
|
xx46 : Nat := 0
|
|
xx47 : Nat := 0
|
|
xx48 : Nat := 0
|
|
xx49 : Nat := 0
|
|
xx50 : Nat := 0
|
|
xx51 : Nat := 0
|
|
xx52 : Nat := 0
|
|
xx53 : Nat := 0
|
|
xx54 : Nat := 0
|
|
xx55 : Nat := 0
|
|
xx56 : Nat := 0
|
|
xx57 : Nat := 0
|
|
xx58 : Nat := 0
|
|
xx59 : Nat := 0
|
|
xx60 : Nat := 0
|
|
|
|
@[noinline] def mkFoo (y : Nat) : Foo :=
|
|
{ y60 := y }
|
|
|
|
#eval (mkFoo 10).y60
|