Mutual records

[bollu]

Try to add support for records that can be mutually defined with inductives. this cleans up many definitions in lean-mlir

This allows for code such as:

mutual

-- | allow structures in mutual inductive blocks.
structure Foo where
  int: Int
  bar: Bar

inductive Bar where
| mk: Bar
| foo: Foo -> Bar
end


#print Foo
#print Bar
def fooBar : Foo := { int := 0, bar := (Bar.mk) }
#check fooBar

which produces the output:

inductive Foo.{u_1} : Type u_1
number of parameters: 0
constructors:
Foo.mk : Int → Bar → Foo

inductive Bar.{u_1} : Type u_1
number of parameters: 0
constructors:
Bar.mk : Bar
Bar.foo : {Foo : Sort u_1} → Foo → Bar

fooBar : Foo

[github-actions]

Thanks for your contribution! Please make sure to follow our Commit Convention.

[bollu]

Test failures as of 138666:

90% tests passed, 136 tests failed out of 1344

Total Test time (real) = 286.62 sec

The following tests FAILED:
	  8 - leantest_1007.lean (Failed)
	 23 - leantest_1098.lean (Failed)
	 46 - leantest_343.lean (Failed)
	 50 - leantest_353.lean (Failed)
	 53 - leantest_386.lean (Failed)
	 54 - leantest_389.lean (Failed)
	 60 - leantest_435b.lean (Failed)
	 61 - leantest_439.lean (Failed)
	 64 - leantest_448.lean (Failed)
	 78 - leantest_620.lean (Failed)
	 83 - leantest_653.lean (Failed)
	 88 - leantest_697.lean (Failed)
	 95 - leantest_815b.lean (Failed)
	 98 - leantest_948.lean (Failed)
	108 - leantest_PPInstances.lean (Failed)
	128 - leantest_autoImplicitForbidden.lean (Failed)
	133 - leantest_badBinderName.lean (Failed)
	137 - leantest_binderCacheIssue.lean (Failed)
	138 - leantest_binderCacheIssue2.lean (Failed)
	149 - leantest_cacheIssue.lean (Failed)
	153 - leantest_classBadOutParam.lean (Failed)
	157 - leantest_congrThmIssue.lean (Failed)
	173 - leantest_defaultInstance.lean (Failed)
	178 - leantest_diamond1.lean (Failed)
	179 - leantest_diamond10.lean (Failed)
	180 - leantest_diamond2.lean (Failed)
	182 - leantest_diamond4.lean (Failed)
	183 - leantest_diamond5.lean (Failed)
	184 - leantest_diamond6.lean (Failed)
	185 - leantest_diamond7.lean (Failed)
	186 - leantest_diamond8.lean (Failed)
	187 - leantest_diamond9.lean (Failed)
	194 - leantest_docStr.lean (Failed)
	195 - leantest_eagerCoeExpansion.lean (Failed)
	226 - leantest_heapSort.lean (Failed)
	231 - leantest_implementedByIssue.lean (Failed)
	232 - leantest_implicitLambdaIssue.lean (Failed)
	237 - leantest_inductive1.lean (Failed)
	248 - leantest_isDefEqOffsetBug.lean (Failed)
	295 - leantest_missingExplicitWithForwardNamedDep.lean (Failed)
	300 - leantest_mulcommErrorMessage.lean (Failed)
	302 - leantest_mutualStruct.lean (Failed)
	384 - leantest_struct1.lean (Failed)
	385 - leantest_structAutoBound.lean (Failed)
	400 - leantest_tcloop.lean (Failed)
	427 - leantest_univInference.lean (Failed)
	440 - leantest_zipper.lean (Failed)
	459 - leanruntest_1123.lean (Failed)
	462 - leanruntest_1132.lean (Failed)
	465 - leanruntest_125.lean (Failed)
	473 - leanruntest_270.lean (Failed)
	474 - leanruntest_28.lean (Failed)
	482 - leanruntest_319.lean (Failed)
	483 - leanruntest_326.lean (Failed)
	494 - leanruntest_436.lean (Failed)
	502 - leanruntest_462.lean (Failed)
	510 - leanruntest_492_lean3.lean (Failed)
	514 - leanruntest_509.lean (Failed)
	519 - leanruntest_602.lean (Failed)
	525 - leanruntest_664.lean (Failed)
	534 - leanruntest_790.lean (Failed)
	536 - leanruntest_796.lean (Failed)
	537 - leanruntest_815.lean (Failed)
	552 - leanruntest_972.lean (Failed)
	555 - leanruntest_988.lean (Failed)
	557 - leanruntest_998Export.lean (Failed)
	559 - leanruntest_CoeNew.lean (Failed)
	565 - leanruntest_KyleAlg.lean (Failed)
	566 - leanruntest_KyleAlgAbbrev.lean (Failed)
	568 - leanruntest_Miller1.lean (Failed)
	570 - leanruntest_Ord.lean (Failed)
	571 - leanruntest_PPTopDownAnalyze.lean (Failed)
	572 - leanruntest_Reid1.lean (Failed)
	578 - leanruntest_ac_expr.lean (Failed)
	586 - leanruntest_alg.lean (Failed)
	597 - leanruntest_assertAfterBug.lean (Failed)
	606 - leanruntest_bigop.lean (Failed)
	620 - leanruntest_cdotTests.lean (Failed)
	626 - leanruntest_classAbbrev.lean (Failed)
	642 - leanruntest_constFun2.lean (Failed)
	684 - leanruntest_defaulValueParamIssue.lean (Failed)
	686 - leanruntest_defaultInstBacktrackIssue.lean (Failed)
	693 - leanruntest_derivingInhabited.lean (Failed)
	694 - leanruntest_derivingRpcEncoding.lean (Failed)
	695 - leanruntest_diamond1.lean (Failed)
	696 - leanruntest_diamond2.lean (Failed)
	699 - leanruntest_diamond5.lean (Failed)
	737 - leanruntest_etaStruct.lean (Failed)
	758 - leanruntest_fieldAutoBound.lean (Failed)
	760 - leanruntest_fieldIssue.lean (Failed)
	765 - leanruntest_flat_expr.lean (Failed)
	799 - leanruntest_implicitApplyIssue.lean (Failed)
	803 - leanruntest_ind_cmd_bug.lean (Failed)
	824 - leanruntest_injective.lean (Failed)
	828 - leanruntest_instPatVar.lean (Failed)
	832 - leanruntest_instprio.lean (Failed)
	840 - leanruntest_irreducibleIssue.lean (Failed)
	846 - leanruntest_james1.lean (Failed)
	852 - leanruntest_kronRWIssue.lean (Failed)
	858 - leanruntest_let_Issue.lean (Failed)
	894 - leanruntest_mathport_issue16.lean (Failed)
	895 - leanruntest_matrix.lean (Failed)
	900 - leanruntest_meta2.lean (Failed)
	908 - leanruntest_missingSizeOfArrayGetThm.lean (Failed)
	915 - leanruntest_monotone.lean (Failed)
	916 - leanruntest_mulcomm.lean (Failed)
	944 - leanruntest_noindexAnnotation.lean (Failed)
	945 - leanruntest_noncomp.lean (Failed)
	950 - leanruntest_ofNatNormNum.lean (Failed)
	951 - leanruntest_ofNat_class.lean (Failed)
	966 - leanruntest_pendingInstBug.lean (Failed)
	1015 - leanruntest_shrinkFn.lean (Failed)
	1051 - leanruntest_sizeof1.lean (Failed)
	1053 - leanruntest_sizeof3.lean (Failed)
	1057 - leanruntest_smartUnfoldingBug.lean (Failed)
	1069 - leanruntest_state12.lean (Failed)
	1071 - leanruntest_stateRef.lean (Failed)
	1075 - leanruntest_struct1.lean (Failed)
	1076 - leanruntest_struct2.lean (Failed)
	1077 - leanruntest_struct3.lean (Failed)
	1080 - leanruntest_structInst3.lean (Failed)
	1094 - leanruntest_stuckMVarBug.lean (Failed)
	1107 - leanruntest_synth1.lean (Failed)
	1109 - leanruntest_synthPendingBug.lean (Failed)
	1118 - leanruntest_tcUnivIssue.lean (Failed)
	1128 - leanruntest_tryHeuristicPerfIssue.lean (Failed)
	1129 - leanruntest_tryHeuristicPerfIssue2.lean (Failed)
	1133 - leanruntest_typeclass_append.lean (Failed)
	1134 - leanruntest_typeclass_coerce.lean (Failed)
	1135 - leanruntest_typeclass_diamond.lean (Failed)
	1138 - leanruntest_typeclass_metas_internal_goals1.lean (Failed)
	1139 - leanruntest_typeclass_metas_internal_goals2.lean (Failed)
	1140 - leanruntest_typeclass_metas_internal_goals3.lean (Failed)
	1141 - leanruntest_typeclass_metas_internal_goals4.lean (Failed)
	1142 - leanruntest_typeclass_outparam.lean (Failed)
	1277 - leanpkgtest_deriving (Failed)