max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2021-08-09 14:29:10 -07:00
parent 5ef72057e9
commit 80cf5202b8
15 changed files with 5399 additions and 2471 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
stage0/src/Init/Core.lean generated
View file

@ -284,7 +284,7 @@ theorem iff_iff_implies_and_implies (a b : Prop) : (a ↔ b) ↔ (a → b) ∧ (
theorem Iff.refl (a : Prop) : a ↔ a :=
Iff.intro (fun h => h) (fun h => h)
theorem Iff.rfl {a : Prop} : a ↔ a :=
protected theorem Iff.rfl {a : Prop} : a ↔ a :=
Iff.refl a
theorem Iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c :=

2
stage0/src/Init/Prelude.lean generated
View file

@ -107,7 +107,7 @@ init_quot
inductive HEq {α : Sort u} (a : α) : {β : Sort u} → β → Prop where
| refl {} : HEq a a
@[matchPattern] def HEq.rfl {α : Sort u} {a : α} : HEq a a :=
@[matchPattern] protected def HEq.rfl {α : Sort u} {a : α} : HEq a a :=
HEq.refl a
theorem eq_of_heq {α : Sort u} {a a' : α} (h : HEq a a') : Eq a a' :=

7
stage0/src/Lean/Elab/StructInst.lean generated
View file

@ -749,10 +749,9 @@ partial def tryToSynthesizeDefault (structs : Array Struct) (allStructNames : Ar
pure false
else if h : i < structs.size then do
let struct := structs.get ⟨i, h⟩
let defaultName := struct.structName ++ fieldName ++ `_default
let env ← getEnv
match env.find? defaultName with
| some cinfo@(ConstantInfo.defnInfo defVal) => do
match getDefaultFnForField? (← getEnv) struct.structName fieldName with
| some defFn =>
let cinfo ← getConstInfo defFn
let mctx ← getMCtx
let val? ← mkDefaultValue? struct cinfo
match val? with

114
stage0/src/Lean/Elab/Structure.lean generated
View file

@ -7,6 +7,7 @@ import Lean.Parser.Command
import Lean.Meta.Closure
import Lean.Meta.SizeOf
import Lean.Meta.Injective
import Lean.Meta.Structure
import Lean.Elab.Command
import Lean.Elab.DeclModifiers
import Lean.Elab.DeclUtil
@ -62,7 +63,7 @@ inductive StructFieldKind where
structure StructFieldInfo where
name : Name
declName : Name -- Remark: this field value doesn't matter for fromParent fields.
declName : Name -- Remark: for `fromParent` fields, `declName` is only relevant in the generation of auxiliary "default value" functions.
fvar : Expr
kind : StructFieldKind
inferMod : Bool := false
@ -227,23 +228,30 @@ private def validStructType (type : Expr) : Bool :=
| Expr.sort .. => true
| _ => false
private def checkParentIsStructure (parent : Expr) : TermElabM Name :=
match parent.getAppFn with
| Expr.const c _ _ => do
unless isStructure (← getEnv) c do
throwError "'{c}' is not a structure"
pure c
| _ => throwError "expected structure"
private def findFieldInfo? (infos : Array StructFieldInfo) (fieldName : Name) : Option StructFieldInfo :=
infos.find? fun info => info.name == fieldName
private def containsFieldName (infos : Array StructFieldInfo) (fieldName : Name) : Bool :=
(findFieldInfo? infos fieldName).isSome
register_builtin_option structureDiamondWarning : Bool := {
defValue := true -- TODO: set as false after finishing support for diamonds
descr := "enable/disable warning messages for structure diamonds"
}
/-- Return `some fieldName` if field `fieldName` of the parent structure `parentStructName` is already in `infos` -/
private def findExistingField? (infos : Array StructFieldInfo) (parentStructName : Name) : CoreM (Option Name) := do
let fieldNames := getStructureFieldsFlattened (← getEnv) parentStructName
for fieldName in fieldNames do
if containsFieldName infos fieldName then
return some fieldName
return none
private partial def processSubfields (structDeclName : Name) (parentFVar : Expr) (parentStructName : Name) (subfieldNames : Array Name)
(infos : Array StructFieldInfo) (k : Array StructFieldInfo → TermElabM α) : TermElabM α :=
let rec loop (i : Nat) (infos : Array StructFieldInfo) := do
go 0 infos
where
go (i : Nat) (infos : Array StructFieldInfo) := do
if h : i < subfieldNames.size then
let subfieldName := subfieldNames.get ⟨i, h⟩
if containsFieldName infos subfieldName then
@ -252,31 +260,68 @@ private partial def processSubfields (structDeclName : Name) (parentFVar : Expr)
let type ← inferType val
withLetDecl subfieldName type val fun subfieldFVar =>
/- The following `declName` is only used for creating the `_default` auxiliary declaration name when
its default value is overwritten in the structure. -/
its default value is overwritten in the structure. If the default value is not overwritten, then its value is irrelevant. -/
let declName := structDeclName ++ subfieldName
let infos := infos.push { name := subfieldName, declName, fvar := subfieldFVar, kind := StructFieldKind.fromParent }
loop (i+1) infos
go (i+1) infos
else
k infos
private partial def copyNewFieldsFrom (structDeclName : Name) (infos : Array StructFieldInfo) (parent : Expr) (parentStructName : Name) (k : Array StructFieldInfo → TermElabM α) : TermElabM α := do
let fieldNames := getStructureFieldsFlattened (← getEnv) parentStructName
let rec go (i : Nat) (infos : Array StructFieldInfo) : TermElabM α := do
if h : i < fieldNames.size then
let fieldName := fieldNames.get ⟨i, h⟩
let fieldType ← getFieldType parent fieldName
match (← findFieldInfo? infos fieldName) with
| some existingFieldInfo =>
let existingFieldType ← inferType existingFieldInfo.fvar
unless (← isDefEq fieldType existingFieldType) do
throwError "parent field type mismatch, field '{fieldName}' from parent '{parentStructName}' {← mkHasTypeButIsExpectedMsg fieldType existingFieldType}"
go (i+1) infos
| none =>
/- TODO: we are ignoring the following information from the `fieldName` declaraion at `parentStructName`.
- Binder annotation
- Visibility annotation (private/protected)
- `inferMod`
- Default value.
-/
withLocalDeclD fieldName fieldType fun fieldFVar => do
let fieldDeclName := structDeclName ++ fieldName
let infos := infos.push { name := fieldName, declName := fieldDeclName, fvar := fieldFVar, value? := none,
kind := StructFieldKind.newField, inferMod := false }
go (i+1) infos
else
k infos
go 0 infos
private partial def withParents (view : StructView) (k : Array StructFieldInfo → TermElabM α) : TermElabM α := do
go 0 #[]
where
go (i : Nat) (infos : Array StructFieldInfo) : TermElabM α := do
if h : i < view.parents.size then
let parentStx := view.parents.get ⟨i, h⟩
withRef parentStx do
let parent ← Term.elabType parentStx
let parentStructName ← getStructureName parent
if let some existingFieldName ← findExistingField? infos parentStructName then
if structureDiamondWarning.get (← getOptions) then
logWarning s!"field '{existingFieldName}' from '{parentStructName}' has already been declared"
copyNewFieldsFrom view.declName infos parent parentStructName fun infos => go (i+1) infos
-- TODO: if `class`, then we need to create a let-decl that stores the local instance for the `parentStructure`
else
let toParentName := Name.mkSimple $ "to" ++ parentStructName.eraseMacroScopes.getString! -- erase macro scopes?
if containsFieldName infos toParentName then
throwErrorAt parentStx "field '{toParentName}' has already been declared"
let env ← getEnv
let binfo := if view.isClass && isClass env parentStructName then BinderInfo.instImplicit else BinderInfo.default
withLocalDecl toParentName binfo parent fun parentFVar =>
let infos := infos.push { name := toParentName, declName := view.declName ++ toParentName, fvar := parentFVar, kind := StructFieldKind.subobject }
let subfieldNames := getStructureFieldsFlattened env parentStructName
processSubfields view.declName parentFVar parentStructName subfieldNames infos fun infos => go (i+1) infos
else
k infos
loop 0 infos
private partial def withParents (view : StructView) (i : Nat) (infos : Array StructFieldInfo) (k : Array StructFieldInfo → TermElabM α) : TermElabM α := do
if h : i < view.parents.size then
let parentStx := view.parents.get ⟨i, h⟩
withRef parentStx do
let parent ← Term.elabType parentStx
let parentName ← checkParentIsStructure parent
let toParentName := Name.mkSimple $ "to" ++ parentName.eraseMacroScopes.getString! -- erase macro scopes?
if containsFieldName infos toParentName then
throwErrorAt parentStx "field '{toParentName}' has already been declared"
let env ← getEnv
let binfo := if view.isClass && isClass env parentName then BinderInfo.instImplicit else BinderInfo.default
withLocalDecl toParentName binfo parent fun parentFVar =>
let infos := infos.push { name := toParentName, declName := view.declName ++ toParentName, fvar := parentFVar, kind := StructFieldKind.subobject }
let subfieldNames := getStructureFieldsFlattened env parentName
processSubfields view.declName parentFVar parentName subfieldNames infos fun infos => withParents view (i+1) infos k
else
k infos
private def elabFieldTypeValue (view : StructFieldView) : TermElabM (Option Expr × Option Expr) := do
Term.withAutoBoundImplicit <| Term.elabBinders view.binders.getArgs fun params => do
@ -516,7 +561,7 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do
let type ← Term.elabType view.type
unless validStructType type do throwErrorAt view.type "expected Type"
withRef view.ref do
withParents view 0 #[] fun fieldInfos =>
withParents view fun fieldInfos =>
withFields view.fields 0 fieldInfos fun fieldInfos => do
Term.synthesizeSyntheticMVarsNoPostponing
let u ← getResultUniverse type
@ -554,19 +599,20 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do
let projInstances := instParents.toList.map fun info => info.declName
Term.applyAttributesAt view.declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking
projInstances.forM fun declName => addInstance declName AttributeKind.global (eval_prio default)
-- TODO: we must create `to` functions for the parent structures that have been flattened, and mark them as instances (if class)
let lctx ← getLCtx
let fieldsWithDefault := fieldInfos.filter fun info => info.value?.isSome
let defaultAuxDecls ← fieldsWithDefault.mapM fun info => do
let type ← inferType info.fvar
pure (info.declName ++ `_default, type, info.value?.get!)
/- The `lctx` and `defaultAuxDecls` are used to create the auxiliary `_default` declarations
pure (mkDefaultFnOfProjFn info.declName, type, info.value?.get!)
/- The `lctx` and `defaultAuxDecls` are used to create the auxiliary "default value" declarations
The parameters `params` for these definitions must be marked as implicit, and all others as explicit. -/
let lctx :=
params.foldl (init := lctx) fun (lctx : LocalContext) (p : Expr) =>
lctx.setBinderInfo p.fvarId! BinderInfo.implicit
let lctx :=
fieldInfos.foldl (init := lctx) fun (lctx : LocalContext) (info : StructFieldInfo) =>
if info.isFromParent then lctx -- `fromParent` fields are elaborated as let-decls, and are zeta-expanded when creating `_default`.
if info.isFromParent then lctx -- `fromParent` fields are elaborated as let-decls, and are zeta-expanded when creating "default value" auxiliary functions
else lctx.setBinderInfo info.fvar.fvarId! BinderInfo.default
addDefaults lctx defaultAuxDecls

2
stage0/src/Lean/Expr.lean generated
View file

@ -32,7 +32,7 @@ instance (a b : Literal) : Decidable (a < b) :=
inductive BinderInfo where
| default | implicit | strictImplicit | instImplicit | auxDecl
deriving Inhabited, BEq
deriving Inhabited, BEq, Repr
def BinderInfo.hash : BinderInfo → UInt64
| BinderInfo.default => 947

1
stage0/src/Lean/Meta.lean generated
View file

@ -35,3 +35,4 @@ import Lean.Meta.SortLocalDecls
import Lean.Meta.CollectFVars
import Lean.Meta.GeneralizeVars
import Lean.Meta.Injective
import Lean.Meta.Structure

40
stage0/src/Lean/Meta/Structure.lean generated Normal file
View file

@ -0,0 +1,40 @@
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
Additional helper methods that require `MetaM` infrastructure.
-/
import Lean.Structure
import Lean.Meta.AppBuilder
namespace Lean.Meta
def getStructureName (struct : Expr) : MetaM Name :=
match struct.getAppFn with
| Expr.const declName .. => do
unless isStructure (← getEnv) declName do
throwError "'{declName}' is not a structure"
return declName
| _ => throwError "expected structure"
def getFieldType (structType : Expr) (fieldName : Name) : MetaM Expr := do
let structName ← getStructureName structType
match findField? (← getEnv) structName fieldName with
| some baseStructName =>
match getPathToBaseStructure? (← getEnv) baseStructName structName with
| none => throwError "failed to access field '{fieldName}' of structure '{structName}'"
| some path =>
match getProjFnForField? (← getEnv) baseStructName fieldName with
| none => unreachable!
| some projFn =>
withLocalDeclD `s structType fun struct => do
let mut struct := struct
for toField in path do
struct ← mkAppM toField #[struct]
let fieldVal ← mkAppM projFn #[struct]
let fieldType ← inferType fieldVal
return fieldType
| none => throwError "'{fieldName}' is not a field of structure '{structName}'"
end Lean.Meta

14
stage0/src/Lean/Structure.lean generated
View file

@ -14,6 +14,8 @@ structure StructureFieldInfo where
fieldName : Name
projFn : Name
subobject? : Option Name -- It is `some parentStructName` if it is a subobject, and `parentStructName` is the name of the parent structure
binderInfo : BinderInfo := BinderInfo.default
inferMod : Bool := false -- true if user used the `{}` when declaring the field
deriving Inhabited, Repr
def StructureFieldInfo.lt (i₁ i₂ : StructureFieldInfo) : Bool :=
@ -135,6 +137,18 @@ def getProjFnForField? (env : Environment) (structName : Name) (fieldName : Name
else
none
def mkDefaultFnOfProjFn (projFn : Name) : Name :=
projFn ++ `_default
def getDefaultFnForField? (env : Environment) (structName : Name) (fieldName : Name) : Option Name :=
if let some projName := getProjFnForField? env structName fieldName then
let defFn := mkDefaultFnOfProjFn projName
if env.contains defFn then defFn else none
else
-- Check if we have a default function for a default values overriden by substructure.
let defFn := mkDefaultFnOfProjFn (structName ++ fieldName)
if env.contains defFn then defFn else none
partial def getPathToBaseStructureAux (env : Environment) (baseStructName : Name) (structName : Name) (path : List Name) : Option (List Name) :=
if baseStructName == structName then
some path.reverse

2
stage0/stdlib/CMakeLists.txt generated
View file

File diff suppressed because one or more lines are too long

189
stage0/stdlib/Lean/Elab/StructInst.c generated
View file

@ -15,6 +15,7 @@ extern "C" {
#endif
lean_object* l_List_reverse___rarg(lean_object*);
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_getStructName_throwUnexpectedExpectedType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_getConstInfo___at_Lean_Elab_Term_mkConst___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabStructInstAux___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_mkFieldMap___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_Struct_modifyFields(lean_object*, lean_object*);
@ -122,10 +123,9 @@ lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_expan
lean_object* l_Lean_Elab_Term_StructInst_Struct_allDefault_match__1(lean_object*);
lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabStructInstAux___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_markDefaultMissing(lean_object*);
lean_object* lean_environment_find(lean_object*, lean_object*);
lean_object* l_Lean_addTrace_addTraceOptions(lean_object*);
static lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_mkDefaultValueAux_x3f___closed__1;
lean_object* l_Lean_Elab_Term_StructInst_initFn____x40_Lean_Elab_StructInst___hyg_7707_(lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_initFn____x40_Lean_Elab_StructInst___hyg_7697_(lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_StructInst_expandStructInstExpectedType___closed__2;
lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_mkDefaultValueAux_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Meta_0__Lean_Syntax_isNatLitAux(lean_object*, lean_object*);
@ -407,7 +407,6 @@ uint8_t l_Lean_Expr_isAppOfArity(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_expandParentFields_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_dbg_to_string(lean_object*);
static lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_expandNonAtomicExplicitSource___lambda__1___closed__5;
static lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__2;
lean_object* l_List_mapM___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_expandNumLitFields___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_defaultMissing_x3f(lean_object*);
lean_object* l_Lean_getPathToBaseStructure_x3f(lean_object*, lean_object*, lean_object*);
@ -560,6 +559,7 @@ lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Ela
static lean_object* l_Lean_Elab_Term_StructInst_expandStructInstExpectedType___closed__13;
lean_object* l_Lean_mkApp(lean_object*, lean_object*);
static lean_object* l_List_map___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_expandParentFields___spec__1___closed__1;
lean_object* l_Lean_getDefaultFnForField_x3f(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_mkSubstructSource_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_Struct_source___boxed(lean_object*);
static lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_expandNonAtomicExplicitSource___lambda__1___closed__15;
@ -684,7 +684,6 @@ static lean_object* l_List_mapM___at___private_Lean_Elab_StructInst_0__Lean_Elab
static lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_getStructName_throwUnexpectedExpectedType___closed__1;
lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_expandParentFields(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_isModifyOp_x3f___spec__3___closed__3;
static lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__3;
lean_object* l_Lean_Expr_getAppFn(lean_object*);
static lean_object* l_Lean_Elab_Term_StructInst_formatStruct___closed__2;
static lean_object* l_List_foldlM___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabStruct___spec__3___lambda__1___closed__8;
@ -21477,27 +21476,13 @@ return x_4;
}
else
{
lean_object* x_5;
lean_object* x_5; lean_object* x_6;
lean_dec(x_3);
x_5 = lean_ctor_get(x_1, 0);
lean_inc(x_5);
if (lean_obj_tag(x_5) == 1)
{
lean_object* x_6; lean_object* x_7;
lean_dec(x_3);
lean_dec(x_1);
x_6 = lean_ctor_get(x_5, 0);
lean_inc(x_6);
x_7 = lean_apply_2(x_2, x_5, x_6);
return x_7;
}
else
{
lean_object* x_8;
lean_dec(x_5);
lean_dec(x_2);
x_8 = lean_apply_1(x_3, x_1);
return x_8;
}
x_6 = lean_apply_1(x_2, x_5);
return x_6;
}
}
}
@ -21533,24 +21518,6 @@ static lean_object* _init_l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthes
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("_default");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___lambda__1___boxed), 1, 0);
return x_1;
}
@ -21589,46 +21556,48 @@ return x_20;
}
else
{
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30;
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_21 = lean_array_fget(x_1, x_6);
x_22 = l_Lean_Elab_Term_StructInst_Struct_structName(x_21);
lean_inc(x_4);
x_23 = l_Lean_Name_append(x_22, x_4);
x_22 = lean_st_ref_get(x_13, x_14);
x_23 = lean_ctor_get(x_22, 0);
lean_inc(x_23);
x_24 = lean_ctor_get(x_22, 1);
lean_inc(x_24);
lean_dec(x_22);
x_24 = l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__2;
x_25 = l_Lean_Name_append(x_23, x_24);
x_25 = lean_ctor_get(x_23, 0);
lean_inc(x_25);
lean_dec(x_23);
x_26 = lean_st_ref_get(x_13, x_14);
x_27 = lean_ctor_get(x_26, 0);
lean_inc(x_27);
x_28 = lean_ctor_get(x_26, 1);
lean_inc(x_28);
lean_dec(x_26);
x_29 = lean_ctor_get(x_27, 0);
lean_inc(x_29);
lean_dec(x_27);
x_30 = lean_environment_find(x_29, x_25);
if (lean_obj_tag(x_30) == 0)
x_26 = l_Lean_Elab_Term_StructInst_Struct_structName(x_21);
lean_inc(x_4);
x_27 = l_Lean_getDefaultFnForField_x3f(x_25, x_26, x_4);
if (lean_obj_tag(x_27) == 0)
{
lean_object* x_31; lean_object* x_32;
lean_object* x_28; lean_object* x_29;
lean_dec(x_21);
x_31 = lean_unsigned_to_nat(1u);
x_32 = lean_nat_add(x_6, x_31);
x_28 = lean_unsigned_to_nat(1u);
x_29 = lean_nat_add(x_6, x_28);
lean_dec(x_6);
x_6 = x_32;
x_14 = x_28;
x_6 = x_29;
x_14 = x_24;
goto _start;
}
else
{
lean_object* x_34;
x_34 = lean_ctor_get(x_30, 0);
lean_inc(x_34);
lean_dec(x_30);
if (lean_obj_tag(x_34) == 1)
lean_object* x_31; lean_object* x_32;
x_31 = lean_ctor_get(x_27, 0);
lean_inc(x_31);
lean_dec(x_27);
lean_inc(x_8);
x_32 = l_Lean_getConstInfo___at_Lean_Elab_Term_mkConst___spec__1(x_31, x_8, x_9, x_10, x_11, x_12, x_13, x_24);
if (lean_obj_tag(x_32) == 0)
{
lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41;
x_35 = lean_st_ref_get(x_13, x_28);
lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41;
x_33 = lean_ctor_get(x_32, 0);
lean_inc(x_33);
x_34 = lean_ctor_get(x_32, 1);
lean_inc(x_34);
lean_dec(x_32);
x_35 = lean_st_ref_get(x_13, x_34);
x_36 = lean_ctor_get(x_35, 1);
lean_inc(x_36);
lean_dec(x_35);
@ -21645,8 +21614,8 @@ lean_inc(x_13);
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_10);
x_41 = l_Lean_Elab_Term_StructInst_DefaultFields_mkDefaultValue_x3f(x_21, x_34, x_8, x_9, x_10, x_11, x_12, x_13, x_39);
lean_dec(x_34);
x_41 = l_Lean_Elab_Term_StructInst_DefaultFields_mkDefaultValue_x3f(x_21, x_33, x_8, x_9, x_10, x_11, x_12, x_13, x_39);
lean_dec(x_33);
lean_dec(x_21);
if (lean_obj_tag(x_41) == 0)
{
@ -21699,7 +21668,7 @@ x_55 = lean_ctor_get(x_53, 1);
lean_inc(x_55);
lean_dec(x_53);
x_56 = 8192;
x_57 = l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__3;
x_57 = l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__1;
x_58 = l_Lean_Expr_FindImpl_initCache;
lean_inc(x_54);
x_59 = l_Lean_Expr_FindImpl_findM_x3f_visit(x_57, x_56, x_54, x_58);
@ -21875,7 +21844,7 @@ x_95 = lean_ctor_get(x_93, 1);
lean_inc(x_95);
lean_dec(x_93);
x_96 = 8192;
x_97 = l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__3;
x_97 = l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__1;
x_98 = l_Lean_Expr_FindImpl_initCache;
lean_inc(x_94);
x_99 = l_Lean_Expr_FindImpl_findM_x3f_visit(x_97, x_96, x_94, x_98);
@ -22068,22 +22037,8 @@ return x_133;
}
else
{
lean_object* x_134; lean_object* x_135;
lean_dec(x_34);
uint8_t x_134;
lean_dec(x_21);
x_134 = lean_unsigned_to_nat(1u);
x_135 = lean_nat_add(x_6, x_134);
lean_dec(x_6);
x_6 = x_135;
x_14 = x_28;
goto _start;
}
}
}
}
else
{
uint8_t x_137; lean_object* x_138; lean_object* x_139;
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
@ -22095,12 +22050,48 @@ lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
x_137 = 0;
x_138 = lean_box(x_137);
x_139 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_139, 0, x_138);
lean_ctor_set(x_139, 1, x_14);
return x_139;
x_134 = !lean_is_exclusive(x_32);
if (x_134 == 0)
{
return x_32;
}
else
{
lean_object* x_135; lean_object* x_136; lean_object* x_137;
x_135 = lean_ctor_get(x_32, 0);
x_136 = lean_ctor_get(x_32, 1);
lean_inc(x_136);
lean_inc(x_135);
lean_dec(x_32);
x_137 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_137, 0, x_135);
lean_ctor_set(x_137, 1, x_136);
return x_137;
}
}
}
}
}
else
{
uint8_t x_138; lean_object* x_139; lean_object* x_140;
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
x_138 = 0;
x_139 = lean_box(x_138);
x_140 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_140, 0, x_139);
lean_ctor_set(x_140, 1, x_14);
return x_140;
}
}
}
@ -22157,7 +22148,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_getStructSource___closed__4;
x_2 = l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__1;
x_3 = lean_unsigned_to_nat(781u);
x_3 = lean_unsigned_to_nat(780u);
x_4 = lean_unsigned_to_nat(25u);
x_5 = l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_getStructSource___closed__6;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -25469,7 +25460,7 @@ x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
lean_object* l_Lean_Elab_Term_StructInst_initFn____x40_Lean_Elab_StructInst___hyg_7707_(lean_object* x_1) {
lean_object* l_Lean_Elab_Term_StructInst_initFn____x40_Lean_Elab_StructInst___hyg_7697_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -25947,10 +25938,6 @@ l_Lean_Elab_Term_StructInst_DefaultFields_reduce___boxed__const__1 = _init_l_Lea
lean_mark_persistent(l_Lean_Elab_Term_StructInst_DefaultFields_reduce___boxed__const__1);
l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__1 = _init_l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__1);
l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__2 = _init_l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__2();
lean_mark_persistent(l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__2);
l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__3 = _init_l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__3();
lean_mark_persistent(l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__3);
l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__1 = _init_l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__1();
lean_mark_persistent(l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__1);
l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__2 = _init_l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__2();
@ -26000,7 +25987,7 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_StructInst_elabStructInst___c
res = l___regBuiltin_Lean_Elab_Term_StructInst_elabStructInst(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = l_Lean_Elab_Term_StructInst_initFn____x40_Lean_Elab_StructInst___hyg_7707_(lean_io_mk_world());
res = l_Lean_Elab_Term_StructInst_initFn____x40_Lean_Elab_StructInst___hyg_7697_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));

4784
stage0/stdlib/Lean/Elab/Structure.c generated
View file

File diff suppressed because it is too large Load diff

578
stage0/stdlib/Lean/Expr.c generated
View file

@ -56,6 +56,7 @@ uint8_t l_UInt64_decEq(uint64_t, uint64_t);
static lean_object* l_Lean_Expr_bindingDomain_x21___closed__2;
lean_object* l_Lean_Expr_abstract___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_Expr_getRevArg_x21___closed__1;
static lean_object* l_Lean_instReprBinderInfo___closed__1;
static lean_object* l_Lean_mkNatLit___closed__1;
lean_object* l_Lean_Expr_isAtomic_match__1(lean_object*);
lean_object* l_Lean_Expr_updateConst___boxed(lean_object*, lean_object*, lean_object*);
@ -134,10 +135,12 @@ lean_object* l_Lean_ExprStructEq_beq_match__1(lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprLiteral____x40_Lean_Expr___hyg_98____closed__6;
uint8_t l_Lean_Level_hasMVar(lean_object*);
lean_object* l_Lean_Expr_constName_x21___boxed(lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__12;
lean_object* l_Lean_Expr_isArrow___boxed(lean_object*);
lean_object* l_Lean_Expr_withAppRev___rarg(lean_object*, lean_object*);
static uint64_t l_Lean_Expr_mkData___closed__3;
lean_object* l_Lean_annotation_x3f___boxed(lean_object*, lean_object*);
lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365__match__1(lean_object*);
uint64_t l_Lean_Expr_mkDataForBinder(uint64_t, lean_object*, uint8_t, uint8_t, uint8_t, uint8_t, uint8_t);
uint8_t lean_name_eq(lean_object*, lean_object*);
lean_object* l_Lean_Expr_setPPExplicit(lean_object*, uint8_t);
@ -176,7 +179,9 @@ static lean_object* l_Lean_Literal_type___closed__3;
lean_object* l_Lean_Expr_isLet_match__1(lean_object*);
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__26;
lean_object* lean_expr_lift_loose_bvars(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__3;
uint8_t lean_expr_has_level_mvar(lean_object*);
static lean_object* l_Lean_ExprStructEq_instBEqExprStructEq___closed__1;
static lean_object* l_Lean_Expr_updateForall_x21___closed__1;
@ -194,22 +199,28 @@ uint8_t l_Lean_Level_hasParam(lean_object*);
lean_object* l_Lean_Expr_updateApp_x21(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_mkAppRevRange(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_isHeadBetaTargetFn_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__14;
lean_object* l_Lean_Expr_updateForall_x21___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_appArg_x21(lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__28;
static lean_object* l_Lean_Expr_fvarId_x21___closed__2;
uint8_t lean_expr_lt(lean_object*, lean_object*);
lean_object* l_Lean_Expr_getRevArg_x21(lean_object*, lean_object*);
static lean_object* l_Lean_Expr_letName_x21___closed__1;
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__5;
lean_object* l_Lean_Expr_getRevArgD_match__1(lean_object*);
lean_object* l_Lean_Expr_replaceFVars(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__30;
static lean_object* l___private_Lean_Expr_0__Lean_reprLiteral____x40_Lean_Expr___hyg_98____closed__4;
uint8_t l_USize_decLt(size_t, size_t);
lean_object* l_Lean_Expr_letName_x21___boxed(lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__18;
lean_object* l_Lean_instCoeExprExprStructEq___boxed(lean_object*);
static lean_object* l_Lean_Expr_updateForall_x21___closed__3;
lean_object* l_Lean_Expr_updateForall_x21(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_List_map___at_Lean_Expr_instantiateLevelParamsArray___spec__4(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_looseBVarRange___boxed(lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__15;
lean_object* l_Lean_Expr_isNatLit_match__1(lean_object*);
lean_object* l_Lean_Expr_mkDataForBinder___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_BinderInfo_hash___boxed(lean_object*);
@ -234,13 +245,14 @@ lean_object* l_Lean_Expr_bindingName_x21___boxed(lean_object*);
static lean_object* l_Lean_Expr_updateLambdaE_x21___closed__1;
lean_object* l_Lean_Expr_getAppFn___boxed(lean_object*);
lean_object* l_Lean_Expr_isBinding_match__1(lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__7;
lean_object* l_Lean_Expr_inferImplicit_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_expr_has_loose_bvar(lean_object*, lean_object*);
lean_object* l_Lean_mkAppN(lean_object*, lean_object*);
lean_object* l_Lean_Expr_natLit_x3f___boxed(lean_object*);
lean_object* l_Lean_mkMData(lean_object*, lean_object*);
lean_object* l_Lean_BinderInfo_hash_match__1(lean_object*);
lean_object* l_Lean_Expr_instantiateLevelParamsCore(lean_object*, lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__11;
lean_object* l_Lean_Expr_updateFn___boxed(lean_object*, lean_object*);
lean_object* l_Lean_mkDecIsTrue(lean_object*, lean_object*);
extern uint64_t l_instInhabitedUInt64;
@ -252,7 +264,9 @@ uint8_t l_Lean_Expr_Data_hasExprMVar(uint64_t);
lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Literal_type(lean_object*);
lean_object* l___private_Lean_Expr_0__Lean_Expr_getParamSubstArray(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__19;
static lean_object* l_Lean_Expr_bindingName_x21___closed__3;
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__25;
lean_object* l_Lean_Expr_hasLooseBVarInExplicitDomain___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_isConstOf___boxed(lean_object*, lean_object*);
lean_object* lean_expr_mk_mdata(lean_object*, lean_object*);
@ -267,17 +281,19 @@ lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l___private_Lean_Expr_0__Lean_reprLiteral____x40_Lean_Expr___hyg_98_(lean_object*, lean_object*);
lean_object* l___private_Lean_Expr_0__Lean_beqBinderInfo____x40_Lean_Expr___hyg_312____boxed(lean_object*, lean_object*);
lean_object* l_Lean_Expr_isProj_match__1(lean_object*);
lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____boxed(lean_object*, lean_object*);
static lean_object* l_Lean_Expr_updateForall_x21___closed__2;
static lean_object* l_Lean_Expr_updateLambdaE_x21___closed__2;
lean_object* l_Lean_mkProj(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Expr_getOptParamDefault_x3f___closed__2;
lean_object* l_Lean_BinderInfo_hash_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_inferImplicit_match__1___rarg(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_instantiate_rev_range(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_updateFn(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
uint8_t l_Lean_ExprStructEq_beq(lean_object*, lean_object*);
lean_object* l_Lean_Expr_updateApp___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__29;
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__1;
lean_object* l_Lean_ExprStructEq_beq___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Level_instantiateParams___at_Lean_Expr_instantiateLevelParams___spec__2___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux_match__1(lean_object*);
@ -294,11 +310,13 @@ lean_object* l_Lean_Expr_constLevels_x21(lean_object*);
lean_object* l_Lean_Expr_hasLevelParam___boxed(lean_object*);
lean_object* l_Lean_Expr_isConst_match__1(lean_object*);
lean_object* l_Lean_Expr_getRevArg_x21_match__1(lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__2;
lean_object* l_Lean_Expr_isConstOf_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_isLambda_match__1(lean_object*);
uint8_t lean_expr_has_mvar(lean_object*);
lean_object* l_Lean_mkRawNatLit(lean_object*);
static lean_object* l_Lean_mkNatLit___closed__6;
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__22;
uint8_t l_Lean_KVMap_getBool(lean_object*, lean_object*, uint8_t);
static lean_object* l_Lean_Expr_ctorName___closed__5;
lean_object* l___private_Lean_Expr_0__Lean_Expr_mkAppRevRangeAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -308,14 +326,17 @@ lean_object* l_Lean_Expr_instantiateLevelParamsCore_visit_match__1___rarg(lean_o
lean_object* l_Lean_BinderInfo_isInstImplicit_match__1(lean_object*);
lean_object* l_Lean_Expr_replaceFVar(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_headBeta(lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__4;
uint8_t lean_expr_binder_info(lean_object*);
static uint64_t l_Lean_Expr_mkData___closed__2;
lean_object* lean_level_update_max(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__27;
lean_object* l_Lean_mkAnnotation(lean_object*, lean_object*);
lean_object* l_Lean_Expr_isLit_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_isHeadBetaTargetFn_match__1(lean_object*);
uint8_t l_Lean_BinderInfo_isStrictImplicit(uint8_t);
lean_object* l_Lean_Expr_isMData_match__1___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__9;
lean_object* l_Lean_Expr_looseBVarRangeEx___boxed(lean_object*);
uint8_t l_Lean_Expr_hasExprMVar(lean_object*);
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
@ -332,6 +353,7 @@ lean_object* l___private_Lean_Expr_0__Lean_Expr_getParamSubstArray___boxed(lean_
uint8_t l_Lean_Expr_isHeadBetaTarget(lean_object*);
uint8_t l_Lean_Expr_isBinding(lean_object*);
lean_object* l_Lean_Expr_bindingBody_x21___boxed(lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__8;
lean_object* l_Lean_Expr_updateProj_x21(lean_object*, lean_object*);
lean_object* l_Lean_Level_instantiateParams___at_Lean_Expr_instantiateLevelParams___spec__3(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_mkDecIsTrue___closed__1;
@ -339,14 +361,17 @@ lean_object* l_Lean_Expr_instantiateLevelParams(lean_object*, lean_object*, lean
lean_object* l_Lean_instDecidableLt___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAutoParamTactic_x3f___boxed(lean_object*);
lean_object* l_Lean_Expr_isForall_match__1(lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__17;
lean_object* l_Lean_BinderInfo_isExplicit_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_Data_hasLevelParam___boxed(lean_object*);
lean_object* l_Lean_Expr_isFVar___boxed(lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Expr_setAppPPExplicitForExposingMVars___spec__1(size_t, size_t, lean_object*);
uint64_t l_Lean_Name_hash(lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__23;
lean_object* l_Nat_repr(lean_object*);
lean_object* l___private_Lean_Expr_0__Lean_Expr_getParamSubst_match__1(lean_object*);
lean_object* l_List_map___rarg(lean_object*, lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__13;
uint8_t l_Lean_Expr_Data_hasFVar(uint64_t);
lean_object* l_Lean_Expr_getAppNumArgsAux_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Expr_instBEqExpr___closed__1;
@ -373,6 +398,7 @@ lean_object* l_Lean_BinderInfo_isInstImplicit_match__1___rarg___boxed(lean_objec
lean_object* l_Lean_Expr_instantiateLevelParamsCore_visit___at_Lean_Expr_instantiateLevelParams___spec__1___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Expr_ctorName___closed__3;
lean_object* l_Lean_Expr_hasAnyFVar_visit___at_Lean_Expr_containsFVar___spec__1___boxed(lean_object*, lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__21;
lean_object* l_Lean_Expr_natLit_x3f(lean_object*);
lean_object* lean_expr_mk_const(lean_object*, lean_object*);
lean_object* l_Lean_Expr_data_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -400,6 +426,7 @@ lean_object* l_Lean_Expr_hasAnyFVar_visit_match__1___rarg(lean_object*, lean_obj
static lean_object* l_Lean_Literal_type___closed__2;
lean_object* l_Lean_Expr_mkDataForLet___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_instantiate___boxed(lean_object*, lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__6;
uint8_t l___private_Lean_Expr_0__Lean_beqLiteral____x40_Lean_Expr___hyg_30_(lean_object*, lean_object*);
static lean_object* l_Lean_mkSimpleThunk___closed__1;
lean_object* l___private_Lean_Expr_0__Lean_reprLiteral____x40_Lean_Expr___hyg_98__match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -407,7 +434,6 @@ static lean_object* l_Lean_Expr_appFn_x21___closed__1;
static lean_object* l_Lean_Expr_updateApp_x21___closed__1;
lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_isConst(lean_object*);
lean_object* l_Lean_BinderInfo_hash_match__1___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_hasLevelMVar(lean_object*);
lean_object* lean_expr_mk_let(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_isConstOf(lean_object*, lean_object*);
@ -472,6 +498,7 @@ static lean_object* l_Lean_Expr_ctorName___closed__9;
lean_object* l_Lean_Expr_instantiateRevRange___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_hasLooseBVarInExplicitDomain_match__1___rarg(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
static lean_object* l_Lean_mkNatLit___closed__7;
lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365_(uint8_t, lean_object*);
uint8_t l_Lean_instInhabitedBinderInfo;
static lean_object* l_Lean_Expr_updateLambda_x21___closed__1;
lean_object* l_Lean_Expr_mkDataForLet___boxed__const__1;
@ -527,6 +554,7 @@ lean_object* l_Lean_Expr_betaRev(lean_object*, lean_object*);
uint64_t l_Lean_instInhabitedData__1;
static lean_object* l_Lean_instBEqLiteral___closed__1;
lean_object* l_Lean_instHashableBinderInfo;
lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365__match__1___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_BinderInfo_isInstImplicit___boxed(lean_object*);
extern lean_object* l_Lean_KVMap_empty;
lean_object* l_Lean_Expr_isLambda_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -565,6 +593,8 @@ static lean_object* l_Lean_Expr_appFn_x21___closed__2;
static lean_object* l_Lean_mkNatLit___closed__5;
lean_object* l_Lean_Expr_Data_hasExprMVar___boxed(lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__5;
lean_object* l_Lean_instReprBinderInfo;
lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365__match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_etaExpanded_x3f(lean_object*);
lean_object* l_Lean_Expr_liftLooseBVars___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Expr_bvarIdx_x21___closed__2;
@ -672,11 +702,13 @@ lean_object* l_Lean_Expr_setOption___at_Lean_Expr_setPPExplicit___spec__1___boxe
lean_object* l_Lean_Expr_isAtomic___boxed(lean_object*);
lean_object* l_Lean_Expr_getAppNumArgsAux_match__1(lean_object*);
lean_object* l_Lean_Expr_Data_nonDepLet___boxed(lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__20;
lean_object* l_Lean_mkNatLit(lean_object*);
lean_object* l_Lean_Level_instantiateParams(lean_object*, lean_object*);
lean_object* l_Lean_mkStrLit(lean_object*);
lean_object* l_Lean_Expr_getArgD(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppFn(lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__10;
lean_object* l_Lean_Expr_etaExpandedStrict_x3f(lean_object*);
lean_object* l_Lean_Expr_updateLambdaE_x21(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_hasLooseBVar___boxed(lean_object*, lean_object*);
@ -695,6 +727,7 @@ static lean_object* l_Lean_instBEqBinderInfo___closed__1;
lean_object* l___private_Lean_Expr_0__Lean_beqLiteral____x40_Lean_Expr___hyg_30__match__1(lean_object*);
lean_object* lean_expr_update_app(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Expr_isCharLit___closed__2;
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__24;
lean_object* l_Lean_Expr_setOption___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_instantiateLevelParamsCore_visit___at_Lean_Expr_instantiateLevelParams___spec__1(lean_object*, lean_object*, lean_object*);
uint64_t l_Lean_BinderInfo_hash(uint8_t);
@ -714,6 +747,7 @@ lean_object* l_Lean_Expr_equal___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Expr_updateLet_x21(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Literal_lt(lean_object*, lean_object*);
lean_object* l_Lean_Expr_updateForall___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__16;
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
lean_object* l_Lean_Expr_bindingInfo_x21___boxed(lean_object*);
lean_object* l_Lean_mkSimpleThunk(lean_object*);
@ -1624,7 +1658,7 @@ x_1 = l_Lean_instBEqBinderInfo___closed__1;
return x_1;
}
}
lean_object* l_Lean_BinderInfo_hash_match__1___rarg(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365__match__1___rarg(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
switch (x_1) {
@ -1686,24 +1720,488 @@ return x_16;
}
}
}
lean_object* l_Lean_BinderInfo_hash_match__1(lean_object* x_1) {
lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365__match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_BinderInfo_hash_match__1___rarg___boxed), 6, 0);
x_2 = lean_alloc_closure((void*)(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365__match__1___rarg___boxed), 6, 0);
return x_2;
}
}
lean_object* l_Lean_BinderInfo_hash_match__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365__match__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
uint8_t x_7; lean_object* x_8;
x_7 = lean_unbox(x_1);
lean_dec(x_1);
x_8 = l_Lean_BinderInfo_hash_match__1___rarg(x_7, x_2, x_3, x_4, x_5, x_6);
x_8 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365__match__1___rarg(x_7, x_2, x_3, x_4, x_5, x_6);
return x_8;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Lean.BinderInfo.default");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__1;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Expr_0__Lean_reprLiteral____x40_Lean_Expr___hyg_98____closed__4;
x_2 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__2;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__4() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__3;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Expr_0__Lean_reprLiteral____x40_Lean_Expr___hyg_98____closed__5;
x_2 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__2;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__6() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__5;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__7() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Lean.BinderInfo.implicit");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__7;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Expr_0__Lean_reprLiteral____x40_Lean_Expr___hyg_98____closed__4;
x_2 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__8;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__10() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__9;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Expr_0__Lean_reprLiteral____x40_Lean_Expr___hyg_98____closed__5;
x_2 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__8;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__12() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__11;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__13() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Lean.BinderInfo.strictImplicit");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__14() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__13;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__15() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Expr_0__Lean_reprLiteral____x40_Lean_Expr___hyg_98____closed__4;
x_2 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__14;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__16() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__15;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__17() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Expr_0__Lean_reprLiteral____x40_Lean_Expr___hyg_98____closed__5;
x_2 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__14;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__18() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__17;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__19() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Lean.BinderInfo.instImplicit");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__20() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__19;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__21() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Expr_0__Lean_reprLiteral____x40_Lean_Expr___hyg_98____closed__4;
x_2 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__20;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__22() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__21;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__23() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Expr_0__Lean_reprLiteral____x40_Lean_Expr___hyg_98____closed__5;
x_2 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__20;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__24() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__23;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__25() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Lean.BinderInfo.auxDecl");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__26() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__25;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__27() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Expr_0__Lean_reprLiteral____x40_Lean_Expr___hyg_98____closed__4;
x_2 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__26;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__28() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__27;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__29() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Expr_0__Lean_reprLiteral____x40_Lean_Expr___hyg_98____closed__5;
x_2 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__26;
x_3 = lean_alloc_ctor(3, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__30() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
x_1 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__29;
x_2 = 0;
x_3 = lean_alloc_ctor(5, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
}
}
lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365_(uint8_t x_1, lean_object* x_2) {
_start:
{
switch (x_1) {
case 0:
{
lean_object* x_3; uint8_t x_4;
x_3 = lean_unsigned_to_nat(1024u);
x_4 = lean_nat_dec_le(x_3, x_2);
if (x_4 == 0)
{
lean_object* x_5; lean_object* x_6;
x_5 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__4;
x_6 = l_Repr_addAppParen(x_5, x_2);
return x_6;
}
else
{
lean_object* x_7; lean_object* x_8;
x_7 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__6;
x_8 = l_Repr_addAppParen(x_7, x_2);
return x_8;
}
}
case 1:
{
lean_object* x_9; uint8_t x_10;
x_9 = lean_unsigned_to_nat(1024u);
x_10 = lean_nat_dec_le(x_9, x_2);
if (x_10 == 0)
{
lean_object* x_11; lean_object* x_12;
x_11 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__10;
x_12 = l_Repr_addAppParen(x_11, x_2);
return x_12;
}
else
{
lean_object* x_13; lean_object* x_14;
x_13 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__12;
x_14 = l_Repr_addAppParen(x_13, x_2);
return x_14;
}
}
case 2:
{
lean_object* x_15; uint8_t x_16;
x_15 = lean_unsigned_to_nat(1024u);
x_16 = lean_nat_dec_le(x_15, x_2);
if (x_16 == 0)
{
lean_object* x_17; lean_object* x_18;
x_17 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__16;
x_18 = l_Repr_addAppParen(x_17, x_2);
return x_18;
}
else
{
lean_object* x_19; lean_object* x_20;
x_19 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__18;
x_20 = l_Repr_addAppParen(x_19, x_2);
return x_20;
}
}
case 3:
{
lean_object* x_21; uint8_t x_22;
x_21 = lean_unsigned_to_nat(1024u);
x_22 = lean_nat_dec_le(x_21, x_2);
if (x_22 == 0)
{
lean_object* x_23; lean_object* x_24;
x_23 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__22;
x_24 = l_Repr_addAppParen(x_23, x_2);
return x_24;
}
else
{
lean_object* x_25; lean_object* x_26;
x_25 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__24;
x_26 = l_Repr_addAppParen(x_25, x_2);
return x_26;
}
}
default:
{
lean_object* x_27; uint8_t x_28;
x_27 = lean_unsigned_to_nat(1024u);
x_28 = lean_nat_dec_le(x_27, x_2);
if (x_28 == 0)
{
lean_object* x_29; lean_object* x_30;
x_29 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__28;
x_30 = l_Repr_addAppParen(x_29, x_2);
return x_30;
}
else
{
lean_object* x_31; lean_object* x_32;
x_31 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__30;
x_32 = l_Repr_addAppParen(x_31, x_2);
return x_32;
}
}
}
}
}
lean_object* l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = lean_unbox(x_1);
lean_dec(x_1);
x_4 = l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365_(x_3, x_2);
lean_dec(x_2);
return x_4;
}
}
static lean_object* _init_l_Lean_instReprBinderInfo___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____boxed), 2, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_instReprBinderInfo() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_instReprBinderInfo___closed__1;
return x_1;
}
}
uint64_t l_Lean_BinderInfo_hash(uint8_t x_1) {
_start:
{
@ -15755,6 +16253,70 @@ l_Lean_instBEqBinderInfo___closed__1 = _init_l_Lean_instBEqBinderInfo___closed__
lean_mark_persistent(l_Lean_instBEqBinderInfo___closed__1);
l_Lean_instBEqBinderInfo = _init_l_Lean_instBEqBinderInfo();
lean_mark_persistent(l_Lean_instBEqBinderInfo);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__1 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__1();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__1);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__2 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__2();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__2);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__3 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__3();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__3);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__4 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__4();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__4);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__5 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__5();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__5);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__6 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__6();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__6);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__7 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__7();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__7);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__8 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__8();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__8);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__9 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__9();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__9);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__10 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__10();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__10);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__11 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__11();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__11);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__12 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__12();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__12);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__13 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__13();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__13);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__14 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__14();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__14);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__15 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__15();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__15);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__16 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__16();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__16);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__17 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__17();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__17);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__18 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__18();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__18);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__19 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__19();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__19);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__20 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__20();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__20);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__21 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__21();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__21);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__22 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__22();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__22);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__23 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__23();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__23);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__24 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__24();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__24);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__25 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__25();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__25);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__26 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__26();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__26);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__27 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__27();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__27);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__28 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__28();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__28);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__29 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__29();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__29);
l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__30 = _init_l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__30();
lean_mark_persistent(l___private_Lean_Expr_0__Lean_reprBinderInfo____x40_Lean_Expr___hyg_365____closed__30);
l_Lean_instReprBinderInfo___closed__1 = _init_l_Lean_instReprBinderInfo___closed__1();
lean_mark_persistent(l_Lean_instReprBinderInfo___closed__1);
l_Lean_instReprBinderInfo = _init_l_Lean_instReprBinderInfo();
lean_mark_persistent(l_Lean_instReprBinderInfo);
l_Lean_instHashableBinderInfo___closed__1 = _init_l_Lean_instHashableBinderInfo___closed__1();
lean_mark_persistent(l_Lean_instHashableBinderInfo___closed__1);
l_Lean_instHashableBinderInfo = _init_l_Lean_instHashableBinderInfo();

6
stage0/stdlib/Lean/Meta.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Meta
// Imports: Init Lean.Meta.Basic Lean.Meta.LevelDefEq Lean.Meta.WHNF Lean.Meta.InferType Lean.Meta.FunInfo Lean.Meta.ExprDefEq Lean.Meta.DiscrTree Lean.Meta.Reduce Lean.Meta.Instances Lean.Meta.AbstractMVars Lean.Meta.SynthInstance Lean.Meta.AppBuilder Lean.Meta.Tactic Lean.Meta.KAbstract Lean.Meta.RecursorInfo Lean.Meta.GeneralizeTelescope Lean.Meta.Match Lean.Meta.ReduceEval Lean.Meta.Closure Lean.Meta.AbstractNestedProofs Lean.Meta.ForEachExpr Lean.Meta.Transform Lean.Meta.PPGoal Lean.Meta.UnificationHint Lean.Meta.Inductive Lean.Meta.SizeOf Lean.Meta.IndPredBelow Lean.Meta.Coe Lean.Meta.SortLocalDecls Lean.Meta.CollectFVars Lean.Meta.GeneralizeVars Lean.Meta.Injective
// Imports: Init Lean.Meta.Basic Lean.Meta.LevelDefEq Lean.Meta.WHNF Lean.Meta.InferType Lean.Meta.FunInfo Lean.Meta.ExprDefEq Lean.Meta.DiscrTree Lean.Meta.Reduce Lean.Meta.Instances Lean.Meta.AbstractMVars Lean.Meta.SynthInstance Lean.Meta.AppBuilder Lean.Meta.Tactic Lean.Meta.KAbstract Lean.Meta.RecursorInfo Lean.Meta.GeneralizeTelescope Lean.Meta.Match Lean.Meta.ReduceEval Lean.Meta.Closure Lean.Meta.AbstractNestedProofs Lean.Meta.ForEachExpr Lean.Meta.Transform Lean.Meta.PPGoal Lean.Meta.UnificationHint Lean.Meta.Inductive Lean.Meta.SizeOf Lean.Meta.IndPredBelow Lean.Meta.Coe Lean.Meta.SortLocalDecls Lean.Meta.CollectFVars Lean.Meta.GeneralizeVars Lean.Meta.Injective Lean.Meta.Structure
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -46,6 +46,7 @@ lean_object* initialize_Lean_Meta_SortLocalDecls(lean_object*);
lean_object* initialize_Lean_Meta_CollectFVars(lean_object*);
lean_object* initialize_Lean_Meta_GeneralizeVars(lean_object*);
lean_object* initialize_Lean_Meta_Injective(lean_object*);
lean_object* initialize_Lean_Meta_Structure(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Lean_Meta(lean_object* w) {
lean_object * res;
@ -150,6 +151,9 @@ lean_dec_ref(res);
res = initialize_Lean_Meta_Injective(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Meta_Structure(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

1108
stage0/stdlib/Lean/Meta/Structure.c generated Normal file
View file

File diff suppressed because it is too large Load diff

1021
stage0/stdlib/Lean/Structure.c generated
View file

File diff suppressed because it is too large Load diff