chore: update stage0
This commit is contained in:
Leonardo de Moura
parent
428fb5be3c
commit
899e11de30
11 changed files with 5985 additions and 3095 deletions
|
|
@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Leonardo de Moura, Sebastian Ullrich
|
||||
-/
|
||||
import Lean.Util.CollectLevelParams
|
||||
import Lean.Elab.DeclUtil
|
||||
import Lean.Elab.Definition
|
||||
import Lean.Elab.Inductive
|
||||
import Lean.Elab.Structure
|
||||
|
|
@ -12,22 +13,6 @@ namespace Lean
|
|||
namespace Elab
|
||||
namespace Command
|
||||
|
||||
def expandOptDeclSig (stx : Syntax) : Syntax × Option Syntax :=
|
||||
-- many Term.bracketedBinder >> Term.optType
|
||||
let binders := stx.getArg 0;
|
||||
let optType := stx.getArg 1; -- optional (parser! " : " >> termParser)
|
||||
if optType.isNone then
|
||||
(binders, none)
|
||||
else
|
||||
let typeSpec := optType.getArg 0;
|
||||
(binders, some $ typeSpec.getArg 1)
|
||||
|
||||
def expandDeclSig (stx : Syntax) : Syntax × Syntax :=
|
||||
-- many Term.bracketedBinder >> Term.typeSpec
|
||||
let binders := stx.getArg 0;
|
||||
let typeSpec := stx.getArg 1;
|
||||
(binders, typeSpec.getArg 1)
|
||||
|
||||
def elabAbbrev (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
|
||||
-- parser! "abbrev " >> declId >> optDeclSig >> declVal
|
||||
let (binders, type) := expandOptDeclSig (stx.getArg 2);
|
||||
|
|
@ -121,26 +106,6 @@ withDeclId declId $ fun name => do
|
|||
applyAttributes stx declName modifiers.attrs AttributeApplicationTime.afterTypeChecking;
|
||||
applyAttributes stx declName modifiers.attrs AttributeApplicationTime.afterCompilation
|
||||
|
||||
private def checkValidInductiveModifier (ref : Syntax) (modifiers : Modifiers) : CommandElabM Unit := do
|
||||
when modifiers.isNoncomputable $
|
||||
throwError ref "invalid use of 'noncomputable' in inductive declaration";
|
||||
when modifiers.isPartial $
|
||||
throwError ref "invalid use of 'partial' in inductive declaration";
|
||||
unless (modifiers.attrs.size == 0 || (modifiers.attrs.size == 1 && (modifiers.attrs.get! 0).name == `class)) $
|
||||
throwError ref "invalid use of attributes in inductive declaration";
|
||||
pure ()
|
||||
|
||||
private def checkValidCtorModifier (ref : Syntax) (modifiers : Modifiers) : CommandElabM Unit := do
|
||||
when modifiers.isNoncomputable $
|
||||
throwError ref "invalid use of 'noncomputable' in constructor declaration";
|
||||
when modifiers.isPartial $
|
||||
throwError ref "invalid use of 'partial' in constructor declaration";
|
||||
when modifiers.isUnsafe $
|
||||
throwError ref "invalid use of 'unsafe' in constructor declaration";
|
||||
when (modifiers.attrs.size != 0) $
|
||||
throwError ref "invalid use of attributes in constructor declaration";
|
||||
pure ()
|
||||
|
||||
/-
|
||||
parser! "inductive " >> declId >> optDeclSig >> many ctor
|
||||
parser! try ("class " >> "inductive ") >> declId >> optDeclSig >> many ctor
|
||||
|
|
@ -185,12 +150,12 @@ inductiveSyntaxToView modifiers decl 2
|
|||
|
||||
def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
|
||||
v ← inductiveSyntaxToView modifiers stx;
|
||||
elabInductiveCore #[v]
|
||||
elabInductiveViews #[v]
|
||||
|
||||
def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
|
||||
let modifiers := modifiers.addAttribute { name := `class };
|
||||
v ← classInductiveSyntaxToView modifiers stx;
|
||||
elabInductiveCore #[v]
|
||||
elabInductiveViews #[v]
|
||||
|
||||
@[builtinCommandElab declaration]
|
||||
def elabDeclaration : CommandElab :=
|
||||
|
|
@ -233,7 +198,7 @@ views ← elems.mapM $ fun stx => do {
|
|||
modifiers ← elabModifiers (stx.getArg 0);
|
||||
inductiveSyntaxToView modifiers (stx.getArg 1)
|
||||
};
|
||||
elabInductiveCore views
|
||||
elabInductiveViews views
|
||||
|
||||
private def isMutualPreambleCommand (stx : Syntax) : Bool :=
|
||||
let k := stx.getKind;
|
||||
|
|
|
|||
|
|
@ -15,6 +15,27 @@ namespace Lean
|
|||
namespace Elab
|
||||
namespace Command
|
||||
|
||||
def checkValidInductiveModifier (ref : Syntax) (modifiers : Modifiers) : CommandElabM Unit := do
|
||||
when modifiers.isNoncomputable $
|
||||
throwError ref "invalid use of 'noncomputable' in inductive declaration";
|
||||
when modifiers.isPartial $
|
||||
throwError ref "invalid use of 'partial' in inductive declaration";
|
||||
unless (modifiers.attrs.size == 0 || (modifiers.attrs.size == 1 && (modifiers.attrs.get! 0).name == `class)) $
|
||||
throwError ref "invalid use of attributes in inductive declaration";
|
||||
pure ()
|
||||
|
||||
def checkValidCtorModifier (ref : Syntax) (modifiers : Modifiers) : CommandElabM Unit := do
|
||||
when modifiers.isNoncomputable $
|
||||
throwError ref "invalid use of 'noncomputable' in constructor declaration";
|
||||
when modifiers.isPartial $
|
||||
throwError ref "invalid use of 'partial' in constructor declaration";
|
||||
when modifiers.isUnsafe $
|
||||
throwError ref "invalid use of 'unsafe' in constructor declaration";
|
||||
when (modifiers.attrs.size != 0) $
|
||||
throwError ref "invalid use of attributes in constructor declaration";
|
||||
pure ()
|
||||
|
||||
|
||||
structure CtorView :=
|
||||
(ref : Syntax)
|
||||
(modifiers : Modifiers)
|
||||
|
|
@ -464,7 +485,7 @@ views.forM fun view => do {
|
|||
pure ()
|
||||
}
|
||||
|
||||
def elabInductiveCore (views : Array InductiveView) : CommandElabM Unit := do
|
||||
def elabInductiveViews (views : Array InductiveView) : CommandElabM Unit := do
|
||||
let view0 := views.get! 0;
|
||||
let ref := view0.ref;
|
||||
decl ← runTermElabM view0.declName $ fun vars => mkInductiveDecl vars views;
|
||||
|
|
|
|||
|
|
@ -5,26 +5,178 @@ Authors: Leonardo de Moura
|
|||
-/
|
||||
import Lean.Elab.Command
|
||||
import Lean.Elab.DeclModifiers
|
||||
import Lean.Elab.DeclUtil
|
||||
import Lean.Elab.Inductive
|
||||
|
||||
namespace Lean
|
||||
namespace Elab
|
||||
namespace Command
|
||||
namespace Structure
|
||||
|
||||
inductive FieldKind
|
||||
| newField | fromParent | subobject
|
||||
/- Recall that the `structure command syntax is
|
||||
```
|
||||
parser! (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >> " := " >> optional structCtor >> structFields
|
||||
```
|
||||
-/
|
||||
|
||||
structure FieldDecl :=
|
||||
(fvar : Expr)
|
||||
(defaultVal? : Option Expr)
|
||||
(hasNewDefault : Bool) -- if true, (re-)declare default value in this structure
|
||||
(kind : FieldKind)
|
||||
(inferMod : Bool)
|
||||
structure StructCtorView :=
|
||||
(ref : Syntax)
|
||||
(modifiers : Modifiers)
|
||||
(inferMod : Bool) -- true if `{}` is used in the constructor declaration
|
||||
(name : Name)
|
||||
(declName : Name)
|
||||
|
||||
end Structure
|
||||
structure StructFieldView :=
|
||||
(ref : Syntax)
|
||||
(modifiers : Modifiers)
|
||||
(binderInfo : BinderInfo)
|
||||
(inferMod : Bool)
|
||||
(declName : Name)
|
||||
(name : Name)
|
||||
(binders : Syntax)
|
||||
(type : Syntax)
|
||||
(value? : Option Syntax)
|
||||
|
||||
def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
|
||||
pure () -- TODO
|
||||
structure StructView :=
|
||||
(ref : Syntax)
|
||||
(modifiers : Modifiers)
|
||||
(scopeLevelNames : List Name) -- All `universe` declarations in the current scope
|
||||
(allUserLevelNames : List Name) -- `scopeLevelNames` ++ explicit universe parameters provided in the `structure` command
|
||||
(declName : Name)
|
||||
(scopeVars : Array Expr) -- All `variable` declaration in the current scope
|
||||
(params : Array Expr) -- Explicit parameters provided in the `structure` command
|
||||
(parents : Array Syntax)
|
||||
(ctor : StructCtorView)
|
||||
(fields : Array StructFieldView)
|
||||
|
||||
structure ElabStructResult :=
|
||||
(decl : Declaration)
|
||||
|
||||
private def defaultCtorName := `mk
|
||||
|
||||
/-
|
||||
The structore constructor syntax is
|
||||
```
|
||||
parser! try (declModifiers >> ident >> optional inferMod >> " :: ")
|
||||
```
|
||||
-/
|
||||
private def expandCtor (structStx : Syntax) (structDeclName : Name) : CommandElabM StructCtorView :=
|
||||
let optCtor := structStx.getArg 6;
|
||||
if optCtor.isNone then
|
||||
pure { ref := structStx, modifiers := {}, inferMod := false, name := defaultCtorName, declName := structDeclName ++ defaultCtorName }
|
||||
else do
|
||||
let ctor := optCtor.getArg 0;
|
||||
modifiers ← elabModifiers (ctor.getArg 0);
|
||||
checkValidCtorModifier ctor modifiers;
|
||||
let inferMod := !(ctor.getArg 2).isNone;
|
||||
let name := ctor.getIdAt 1;
|
||||
let declName := structDeclName ++ name;
|
||||
declName ← applyVisibility ctor modifiers.visibility declName;
|
||||
pure { ref := ctor, name := name, modifiers := modifiers, inferMod := inferMod, declName := declName }
|
||||
|
||||
def checkValidFieldModifier (ref : Syntax) (modifiers : Modifiers) : CommandElabM Unit := do
|
||||
when modifiers.isNoncomputable $
|
||||
throwError ref "invalid use of 'noncomputable' in field declaration";
|
||||
when modifiers.isPartial $
|
||||
throwError ref "invalid use of 'partial' in field declaration";
|
||||
when modifiers.isUnsafe $
|
||||
throwError ref "invalid use of 'unsafe' in field declaration";
|
||||
when (modifiers.attrs.size != 0) $
|
||||
throwError ref "invalid use of attributes in field declaration";
|
||||
pure ()
|
||||
|
||||
/-
|
||||
```
|
||||
def structExplicitBinder := parser! try (declModifiers >> "(") >> many1 ident >> optional inferMod >> declSig >> optional Term.binderDefault >> ")"
|
||||
def structImplicitBinder := parser! try (declModifiers >> "{") >> many1 ident >> optional inferMod >> declSig >> "}"
|
||||
def structInstBinder := parser! try (declModifiers >> "[") >> many1 ident >> optional inferMod >> declSig >> "]"
|
||||
def structFields := parser! many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder)
|
||||
```
|
||||
-/
|
||||
private def expandFields (structStx : Syntax) (structDeclName : Name) : CommandElabM (Array StructFieldView) :=
|
||||
let fieldBinders := (structStx.getArg 7).getArgs;
|
||||
fieldBinders.foldlM
|
||||
(fun (views : Array StructFieldView) fieldBinder => do
|
||||
let k := fieldBinder.getKind;
|
||||
binfo ←
|
||||
if k == `Lean.Parser.Command.structExplicitBinder then pure BinderInfo.default
|
||||
else if k == `Lean.Parser.Command.structImplicitBinder then pure BinderInfo.implicit
|
||||
else if k == `Lean.Parser.Command.structInstBinder then pure BinderInfo.instImplicit
|
||||
else throwError fieldBinder "unexpected kind of structure field";
|
||||
modifiers ← elabModifiers (fieldBinder.getArg 0);
|
||||
checkValidFieldModifier fieldBinder modifiers;
|
||||
let inferMod := !(fieldBinder.getArg 3).isNone;
|
||||
let (binders, type) := expandDeclSig (fieldBinder.getArg 4);
|
||||
let value? :=
|
||||
if binfo != BinderInfo.default then none
|
||||
else
|
||||
let optBinderDefault := fieldBinder.getArg 5;
|
||||
if optBinderDefault.isNone then none
|
||||
else
|
||||
-- binderDefault := parser! " := " >> termParser
|
||||
some $ (optBinderDefault.getArg 0).getArg 1;
|
||||
let idents := (fieldBinder.getArg 2).getArgs;
|
||||
idents.foldlM
|
||||
(fun (views : Array StructFieldView) ident => do
|
||||
let name := ident.getId;
|
||||
let declName := structDeclName ++ name;
|
||||
declName ← applyVisibility ident modifiers.visibility declName;
|
||||
pure $ views.push {
|
||||
ref := fieldBinder,
|
||||
modifiers := modifiers,
|
||||
binderInfo := binfo,
|
||||
inferMod := inferMod,
|
||||
declName := declName,
|
||||
name := name,
|
||||
binders := binders,
|
||||
type := type,
|
||||
value? := value? })
|
||||
views)
|
||||
#[]
|
||||
|
||||
private def elabStructureView (view : StructView) : TermElabM ElabStructResult :=
|
||||
throw $ arbitrary _ -- TODO
|
||||
|
||||
/-
|
||||
parser! (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >> " := " >> optional structCtor >> structFields
|
||||
|
||||
where
|
||||
def «extends» := parser! " extends " >> sepBy1 termParser ", "
|
||||
def typeSpec := parser! " : " >> termParser
|
||||
def optType : Parser := optional typeSpec
|
||||
|
||||
def structFields := parser! many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder)
|
||||
def structCtor := parser! try (declModifiers >> ident >> optional inferMod >> " :: ")
|
||||
|
||||
-/
|
||||
def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
|
||||
checkValidInductiveModifier stx modifiers;
|
||||
let isClass := (stx.getArg 0).getKind == `Lean.Parser.Command.classTk;
|
||||
let modifiers := if isClass then modifiers.addAttribute { name := `class } else modifiers;
|
||||
let declId := stx.getArg 1;
|
||||
let params := (stx.getArg 2).getArgs;
|
||||
let exts := stx.getArg 3;
|
||||
let parents := if exts.isNone then #[] else (exts.getArg 1).getArgs.getSepElems;
|
||||
let optType := stx.getArg 4;
|
||||
type ← if optType.isNone then `(Type _) else pure $ (optType.getArg 0).getArg 1;
|
||||
scopeLevelNames ← getLevelNames;
|
||||
withDeclId declId $ fun name => do
|
||||
declName ← mkDeclName declId modifiers name;
|
||||
allUserLevelNames ← getLevelNames;
|
||||
ctor ← expandCtor stx declName;
|
||||
fields ← expandFields stx declName;
|
||||
r ← runTermElabM declName $ fun scopeVars => Term.elabBinders params $ fun params => elabStructureView {
|
||||
ref := stx,
|
||||
modifiers := modifiers,
|
||||
scopeLevelNames := scopeLevelNames,
|
||||
allUserLevelNames := allUserLevelNames,
|
||||
declName := declName,
|
||||
scopeVars := scopeVars,
|
||||
params := params,
|
||||
parents := parents,
|
||||
ctor := ctor,
|
||||
fields := fields
|
||||
};
|
||||
pure () -- TODO
|
||||
|
||||
end Command
|
||||
end Elab
|
||||
|
|
|
|||
|
|
@ -57,9 +57,9 @@ def inferMod := parser! try ("{" >> "}")
|
|||
def ctor := parser! " | " >> declModifiers >> ident >> optional inferMod >> optDeclSig
|
||||
def «inductive» := parser! "inductive " >> declId >> optDeclSig >> many ctor
|
||||
def classInductive := parser! try ("class " >> "inductive ") >> declId >> optDeclSig >> many ctor
|
||||
def structExplicitBinder := parser! try (declModifiers >> "(") >> many ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
|
||||
def structImplicitBinder := parser! try (declModifiers >> "{") >> many ident >> optional inferMod >> optDeclSig >> "}"
|
||||
def structInstBinder := parser! try (declModifiers >> "[") >> declModifiers >> many ident >> optional inferMod >> optDeclSig >> "]"
|
||||
def structExplicitBinder := parser! try (declModifiers >> "(") >> many1 ident >> optional inferMod >> declSig >> optional Term.binderDefault >> ")"
|
||||
def structImplicitBinder := parser! try (declModifiers >> "{") >> many1 ident >> optional inferMod >> declSig >> "}"
|
||||
def structInstBinder := parser! try (declModifiers >> "[") >> many1 ident >> optional inferMod >> declSig >> "]"
|
||||
def structFields := parser! many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder)
|
||||
def structCtor := parser! try (declModifiers >> ident >> optional inferMod >> " :: ")
|
||||
def structureTk := parser! "structure "
|
||||
|
|
|
|||
|
|
@ -248,7 +248,6 @@ struct structure_cmd_fn {
|
|||
expr m_type;
|
||||
buffer<optional<name>> m_parent_refs;
|
||||
buffer<expr> m_parents;
|
||||
buffer<bool> m_private_parents;
|
||||
name m_mk;
|
||||
name m_mk_short;
|
||||
name m_private_prefix;
|
||||
|
|
@ -256,7 +255,6 @@ struct structure_cmd_fn {
|
|||
implicit_infer_kind m_mk_infer;
|
||||
buffer<field_decl> m_fields;
|
||||
std::vector<rename_vector> m_renames;
|
||||
std::vector<field_map> m_field_maps;
|
||||
bool m_explicit_universe_params;
|
||||
bool m_infer_result_universe;
|
||||
bool m_inductive_predicate;
|
||||
|
|
@ -348,16 +346,13 @@ struct structure_cmd_fn {
|
|||
m_p.next();
|
||||
while (true) {
|
||||
auto pos = m_p.pos();
|
||||
bool is_private_parent = false;
|
||||
if (m_p.curr_is_token(get_private_tk())) {
|
||||
m_p.next();
|
||||
is_private_parent = true;
|
||||
throw parser_error("invalid 'structure' extends, private parent structures are not supported", pos);
|
||||
}
|
||||
pair<optional<name>, expr> qparent = m_p.parse_qualified_expr();
|
||||
m_parent_refs.push_back(qparent.first);
|
||||
expr const & parent = qparent.second;
|
||||
m_parents.push_back(parent);
|
||||
m_private_parents.push_back(is_private_parent);
|
||||
name const & parent_name = check_parent(parent);
|
||||
auto parent_info = get_parent_info(parent_name);
|
||||
unsigned nparams = std::get<1>(parent_info);
|
||||
|
|
@ -550,16 +545,13 @@ struct structure_cmd_fn {
|
|||
});
|
||||
}
|
||||
|
||||
/** \brief Process extends clauses.
|
||||
This method also populates the vector m_field_maps and m_fields. */
|
||||
/** \brief Process extends clauses. */
|
||||
void process_extends() {
|
||||
lean_assert(m_fields.size() == m_parents.size());
|
||||
lean_assert(m_field_maps.empty());
|
||||
|
||||
for (unsigned i = 0; i < m_parents.size(); i++) {
|
||||
expr const & parent = m_parents[i];
|
||||
name const & parent_name = check_parent(parent);
|
||||
m_field_maps.push_back(field_map());
|
||||
buffer<expr> args;
|
||||
expr parent_fn = get_app_args(parent, args);
|
||||
|
||||
|
|
@ -608,7 +600,6 @@ struct structure_cmd_fn {
|
|||
m_fields.emplace_back(subfield, some_expr(proj), field_kind::from_parent);
|
||||
}
|
||||
}
|
||||
lean_assert(m_parents.size() == m_field_maps.size());
|
||||
}
|
||||
|
||||
void instantiate_mvars() {
|
||||
|
|
@ -1059,7 +1050,6 @@ struct structure_cmd_fn {
|
|||
}
|
||||
|
||||
void declare_coercions() {
|
||||
lean_assert(m_parents.size() == m_field_maps.size());
|
||||
buffer<name> coercion_names;
|
||||
mk_coercion_names(coercion_names);
|
||||
names lnames = names(m_level_names);
|
||||
|
|
@ -1070,11 +1060,10 @@ struct structure_cmd_fn {
|
|||
expr const & parent_fn = get_app_args(parent, parent_params);
|
||||
name const & parent_name = const_name(parent_fn);
|
||||
|
||||
if (!m_private_parents[i]) {
|
||||
if (m_meta_info.m_attrs.has_class() && is_class(m_env, parent_name)) {
|
||||
// if both are classes, then we also mark coercion_name as an instance
|
||||
m_env = add_instance(m_env, m_name + m_fields[i].get_name(), true);
|
||||
}
|
||||
|
||||
if (m_meta_info.m_attrs.has_class() && is_class(m_env, parent_name)) {
|
||||
// if both are classes, then we also mark coercion_name as an instance
|
||||
m_env = add_instance(m_env, m_name + m_fields[i].get_name(), true);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1178,7 +1167,6 @@ struct structure_cmd_fn {
|
|||
m_parent_refs.push_back(qparent.first);
|
||||
expr const & parent = qparent.second;*/
|
||||
m_parents.push_back(parent);
|
||||
// m_private_parents.push_back(is_private_parent);
|
||||
name const & parent_name = check_parent(parent);
|
||||
auto parent_info = get_parent_info(parent_name);
|
||||
unsigned nparams = std::get<1>(parent_info);
|
||||
|
|
|
|||
File diff suppressed because one or more lines are too long
104
stage0/stdlib/Lean/Elab/DeclUtil.c
Normal file
104
stage0/stdlib/Lean/Elab/DeclUtil.c
Normal file
|
|
@ -0,0 +1,104 @@
|
|||
// Lean compiler output
|
||||
// Module: Lean.Elab.DeclUtil
|
||||
// Imports: Init
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
#elif defined(__GNUC__) && !defined(__CLANG__)
|
||||
#pragma GCC diagnostic ignored "-Wunused-parameter"
|
||||
#pragma GCC diagnostic ignored "-Wunused-label"
|
||||
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
|
||||
#endif
|
||||
#ifdef __cplusplus
|
||||
extern "C" {
|
||||
#endif
|
||||
lean_object* l_Lean_Elab_expandOptDeclSig(lean_object*);
|
||||
lean_object* l_Lean_Elab_expandOptDeclSig___boxed(lean_object*);
|
||||
lean_object* l_Lean_Elab_expandDeclSig___boxed(lean_object*);
|
||||
lean_object* l_Lean_Elab_expandDeclSig(lean_object*);
|
||||
uint8_t l_Lean_Syntax_isNone(lean_object*);
|
||||
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_expandOptDeclSig(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; uint8_t x_6;
|
||||
x_2 = lean_unsigned_to_nat(0u);
|
||||
x_3 = l_Lean_Syntax_getArg(x_1, x_2);
|
||||
x_4 = lean_unsigned_to_nat(1u);
|
||||
x_5 = l_Lean_Syntax_getArg(x_1, x_4);
|
||||
x_6 = l_Lean_Syntax_isNone(x_5);
|
||||
if (x_6 == 0)
|
||||
{
|
||||
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
|
||||
x_7 = l_Lean_Syntax_getArg(x_5, x_2);
|
||||
lean_dec(x_5);
|
||||
x_8 = l_Lean_Syntax_getArg(x_7, x_4);
|
||||
lean_dec(x_7);
|
||||
x_9 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_9, 0, x_8);
|
||||
x_10 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_10, 0, x_3);
|
||||
lean_ctor_set(x_10, 1, x_9);
|
||||
return x_10;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_11; lean_object* x_12;
|
||||
lean_dec(x_5);
|
||||
x_11 = lean_box(0);
|
||||
x_12 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_12, 0, x_3);
|
||||
lean_ctor_set(x_12, 1, x_11);
|
||||
return x_12;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Elab_expandOptDeclSig___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_Lean_Elab_expandOptDeclSig(x_1);
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Elab_expandDeclSig(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
|
||||
x_2 = lean_unsigned_to_nat(0u);
|
||||
x_3 = l_Lean_Syntax_getArg(x_1, x_2);
|
||||
x_4 = lean_unsigned_to_nat(1u);
|
||||
x_5 = l_Lean_Syntax_getArg(x_1, x_4);
|
||||
x_6 = l_Lean_Syntax_getArg(x_5, x_4);
|
||||
lean_dec(x_5);
|
||||
x_7 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_7, 0, x_3);
|
||||
lean_ctor_set(x_7, 1, x_6);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Elab_expandDeclSig___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_Lean_Elab_expandDeclSig(x_1);
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* initialize_Init(lean_object*);
|
||||
static bool _G_initialized = false;
|
||||
lean_object* initialize_Lean_Elab_DeclUtil(lean_object* w) {
|
||||
lean_object * res;
|
||||
if (_G_initialized) return lean_mk_io_result(lean_box(0));
|
||||
_G_initialized = true;
|
||||
res = initialize_Init(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
return lean_mk_io_result(lean_box(0));
|
||||
}
|
||||
#ifdef __cplusplus
|
||||
}
|
||||
#endif
|
||||
File diff suppressed because it is too large
Load diff
|
|
@ -27,18 +27,20 @@ lean_object* lean_mk_cases_on(lean_object*, lean_object*);
|
|||
extern lean_object* l_Lean_Expr_eq_x3f___closed__2;
|
||||
lean_object* l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___main___closed__18;
|
||||
lean_object* l_Array_forMAux___main___at___private_Lean_Elab_Inductive_4__checkLevelNames___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_checkValidInductiveModifier___closed__6;
|
||||
lean_object* l___private_Lean_Elab_Inductive_21__shouldInferResultUniverse___closed__1;
|
||||
lean_object* l_Lean_Elab_Command_addDecl(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_mkSort(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_mapM___main___at___private_Lean_Elab_Inductive_30__updateParams___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_checkValidInductiveModifier___closed__5;
|
||||
lean_object* l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___main___closed__15;
|
||||
lean_object* l___private_Lean_Elab_Inductive_13__withInductiveLocalDeclsAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Array_iterateMAux___main___at_Lean_ppGoal___spec__6___closed__3;
|
||||
lean_object* l___private_Lean_Elab_Inductive_21__shouldInferResultUniverse___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_unreachable_x21___rarg(lean_object*);
|
||||
lean_object* l_Lean_Meta_isClassExpensive___main(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_elabInductiveCore___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_checkValidCtorModifier___closed__4;
|
||||
extern lean_object* l_Lean_MessageData_ofList___closed__3;
|
||||
uint8_t l_USize_decEq(size_t, size_t);
|
||||
lean_object* lean_array_uget(lean_object*, size_t);
|
||||
|
|
@ -65,7 +67,6 @@ lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
|
|||
lean_object* l_Std_HashMapImp_find_x3f___at_Lean_hasOutParams___spec__5(lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_6__throwUnexpectedInductiveType___rarg___closed__3;
|
||||
lean_object* l___private_Lean_Elab_Inductive_29__withUsed(lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_elabInductiveCore(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_mapM___main___at___private_Lean_Elab_Inductive_33__replaceIndFVarsWithConsts___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_isClassQuick___main(lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Array_empty___closed__1;
|
||||
|
|
@ -89,9 +90,11 @@ lean_object* l___private_Lean_Elab_Inductive_8__eqvFirstTypeResult___lambda__1__
|
|||
lean_object* l___private_Lean_Elab_Inductive_22__addLevel___main(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_1__elabHeaderAux___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_19__getResultingUniverse(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_checkValidCtorModifier___closed__10;
|
||||
lean_object* l_Std_HashMapImp_insert___at___private_Lean_MetavarContext_2__visit___spec__3(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_24__collectUniversesFromCtorType___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_mapM___main___at___private_Lean_Elab_Inductive_16__elabCtors___spec__1(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_forMAux___main___at_Lean_Elab_Command_elabInductiveViews___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_mapM___main___at___private_Lean_Elab_Inductive_17__levelMVarToParamAux___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Command_3__setState(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_21__shouldInferResultUniverse___closed__4;
|
||||
|
|
@ -116,8 +119,10 @@ lean_object* l_List_mapM___main___at___private_Lean_Elab_Inductive_33__replaceIn
|
|||
lean_object* l_List_mapM___main___at___private_Lean_Elab_Inductive_16__elabCtors___spec__1___lambda__1(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_mapM___main___at___private_Lean_Elab_Inductive_16__elabCtors___spec__1___lambda__1___closed__2;
|
||||
lean_object* l___private_Lean_Elab_SyntheticMVars_11__synthesizeSyntheticMVarsAux___main(uint8_t, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_checkValidCtorModifier___closed__9;
|
||||
lean_object* l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___main___closed__14;
|
||||
lean_object* l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___main___closed__10;
|
||||
lean_object* l_Lean_Elab_Command_checkValidCtorModifier___closed__8;
|
||||
lean_object* l___private_Lean_Elab_Inductive_6__throwUnexpectedInductiveType___rarg___closed__2;
|
||||
lean_object* l___private_Lean_Elab_Inductive_31__collectLevelParamsInInductive(lean_object*);
|
||||
lean_object* l_List_mapM___main___at___private_Lean_Elab_Inductive_16__elabCtors___spec__1___lambda__1___closed__9;
|
||||
|
|
@ -134,6 +139,7 @@ lean_object* l___private_Lean_Elab_Inductive_7__getResultingType___lambda__1___b
|
|||
lean_object* l___private_Lean_Elab_Inductive_22__addLevel___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_CtorView_inhabited;
|
||||
extern lean_object* l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
|
||||
lean_object* l_Lean_Elab_Command_checkValidInductiveModifier___closed__7;
|
||||
lean_object* l___private_Lean_Elab_Inductive_6__throwUnexpectedInductiveType___rarg___closed__1;
|
||||
lean_object* l___private_Lean_Elab_Inductive_13__withInductiveLocalDeclsAux___main___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_23__collectUniversesFromCtorTypeAux___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -160,6 +166,7 @@ lean_object* l_List_map___main___at___private_Lean_Elab_Inductive_35__applyInfer
|
|||
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
|
||||
lean_object* l_List_mapM___main___at___private_Lean_Elab_Inductive_16__elabCtors___spec__1___lambda__1___closed__6;
|
||||
lean_object* l___private_Lean_Elab_Inductive_26__updateResultingUniverse(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_forMAux___main___at_Lean_Elab_Command_elabInductiveViews___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_forMAux___main___at___private_Lean_Elab_Inductive_37__mkAuxConstructions___spec__1(uint8_t, uint8_t, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_26__updateResultingUniverse___closed__2;
|
||||
uint8_t l_Lean_Level_isParam(lean_object*);
|
||||
|
|
@ -177,6 +184,7 @@ extern lean_object* l_Lean_Expr_heq_x3f___closed__2;
|
|||
lean_object* l___private_Lean_Elab_Inductive_2__checkNumParams___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_5__mkTypeFor(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_elabInductiveViews(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_22__addLevel(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Std_PersistentHashMap_find_x21___rarg___closed__2;
|
||||
lean_object* l___private_Lean_Elab_Inductive_36__mkInductiveDecl___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*, lean_object*);
|
||||
|
|
@ -193,9 +201,9 @@ lean_object* l___private_Lean_Elab_Inductive_32__mkIndFVar2Const(lean_object*, l
|
|||
lean_object* l___private_Lean_Elab_Inductive_1__elabHeaderAux___main___lambda__1___closed__1;
|
||||
lean_object* l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___main___closed__12;
|
||||
lean_object* l_Lean_Elab_Term_assignLevelMVar(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_forMAux___main___at_Lean_Elab_Command_elabInductiveCore___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_ElabHeaderResult_inhabited___closed__1;
|
||||
lean_object* l_List_map___main___at___private_Lean_Elab_Inductive_26__updateResultingUniverse___spec__2(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_checkValidCtorModifier___closed__11;
|
||||
lean_object* lean_mk_brec_on(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabTermAux___main(lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_1__elabHeaderAux___main___lambda__1___closed__3;
|
||||
|
|
@ -203,6 +211,7 @@ lean_object* l___private_Lean_Elab_Inductive_24__collectUniversesFromCtorType(le
|
|||
lean_object* l_Array_forMAux___main___at___private_Lean_Elab_Inductive_2__checkNumParams___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_8__eqvFirstTypeResult(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_20__tmpIndParam___closed__3;
|
||||
lean_object* l_Lean_Elab_Command_checkValidInductiveModifier___closed__3;
|
||||
lean_object* l___private_Lean_Elab_Inductive_21__shouldInferResultUniverse___closed__2;
|
||||
lean_object* lean_name_mk_string(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_throwError___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -212,6 +221,7 @@ lean_object* l___private_Lean_Elab_Inductive_6__throwUnexpectedInductiveType(lea
|
|||
lean_object* l___private_Lean_Elab_Inductive_21__shouldInferResultUniverse___closed__6;
|
||||
lean_object* l_Array_forMAux___main___at___private_Lean_Elab_Inductive_2__checkNumParams___spec__1___closed__1;
|
||||
lean_object* l_List_map___main___at___private_Lean_Elab_Inductive_26__updateResultingUniverse___spec__3(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_throwError___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_map___main___at___private_Lean_Elab_Inductive_26__updateResultingUniverse___spec__2___lambda__1(lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_1__elabHeaderAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Environment_contains(lean_object*, lean_object*);
|
||||
|
|
@ -224,6 +234,7 @@ lean_object* l___private_Lean_Elab_Inductive_21__shouldInferResultUniverse___clo
|
|||
extern lean_object* l_Lean_Meta_AbstractMVars_abstractExprMVars___main___closed__3;
|
||||
lean_object* l___private_Lean_Elab_Inductive_23__collectUniversesFromCtorTypeAux___main___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_19__getResultingUniverse___closed__1;
|
||||
lean_object* l_Lean_Elab_Command_checkValidCtorModifier___closed__6;
|
||||
lean_object* l___private_Lean_Elab_Inductive_17__levelMVarToParamAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_mk_no_confusion(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_withNewLocalInstances___main___at___private_Lean_Elab_Inductive_33__replaceIndFVarsWithConsts___spec__5(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -244,11 +255,13 @@ lean_object* l_Nat_foldMAux___main___at___private_Lean_Elab_Inductive_36__mkIndu
|
|||
lean_object* l___private_Lean_Elab_Inductive_19__getResultingUniverse___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_mkFVar(lean_object*);
|
||||
uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
|
||||
extern lean_object* l_Lean_registerClassAttr___closed__2;
|
||||
lean_object* l___private_Lean_Elab_Inductive_30__updateParams(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_10__checkHeader(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_1__elabHeaderAux___main___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_withNewLocalInstances___main___at___private_Lean_Elab_Inductive_33__replaceIndFVarsWithConsts___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_19__getResultingUniverse___closed__4;
|
||||
lean_object* l_Lean_Elab_Command_checkValidCtorModifier___closed__2;
|
||||
lean_object* l_Lean_Elab_Command_sortDeclLevelParams(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_1__elabHeaderAux___main___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_expr_update_proj(lean_object*, lean_object*);
|
||||
|
|
@ -269,9 +282,11 @@ lean_object* l___private_Lean_Elab_Inductive_21__shouldInferResultUniverse___clo
|
|||
lean_object* l_List_foldl___main___at___private_Lean_Elab_Inductive_31__collectLevelParamsInInductive___spec__2(lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_36__mkInductiveDecl___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_mapM___main___at___private_Lean_Elab_Inductive_33__replaceIndFVarsWithConsts___spec__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_checkValidCtorModifier___closed__1;
|
||||
lean_object* l_List_foldl___main___at___private_Lean_Elab_Inductive_31__collectLevelParamsInInductive___spec__1(lean_object*, lean_object*);
|
||||
size_t lean_ptr_addr(lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_20__tmpIndParam;
|
||||
lean_object* l_Lean_Elab_Command_checkValidCtorModifier___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at___private_Lean_Elab_Inductive_33__replaceIndFVarsWithConsts___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_34__mkCtor2InferMod___boxed(lean_object*);
|
||||
uint8_t l_Lean_BinderInfo_beq(uint8_t, uint8_t);
|
||||
|
|
@ -292,7 +307,6 @@ lean_object* l___private_Lean_Elab_Inductive_18__levelMVarToParam___boxed(lean_o
|
|||
lean_object* l_Lean_Elab_Command_InductiveView_inhabited___closed__1;
|
||||
lean_object* l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___main___closed__9;
|
||||
lean_object* l_Lean_Syntax_getArgs(lean_object*);
|
||||
lean_object* l_Array_forMAux___main___at_Lean_Elab_Command_elabInductiveCore___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Meta_Basic_4__forallTelescopeReducingAuxAux___main___at___private_Lean_Elab_Inductive_33__replaceIndFVarsWithConsts___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_33__replaceIndFVarsWithConsts(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_forMAux___main___at___private_Lean_Elab_Inductive_4__checkLevelNames___spec__1___closed__1;
|
||||
|
|
@ -307,25 +321,32 @@ extern lean_object* l_Lean_Expr_ReplaceLevelImpl_initCache;
|
|||
extern lean_object* l_Std_HashMap_find_x21___rarg___closed__1;
|
||||
lean_object* l_Array_forMAux___main___at___private_Lean_Elab_Inductive_4__checkLevelNames___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___main___closed__11;
|
||||
extern lean_object* l_Lean_Elab_Command_Attribute_inhabited;
|
||||
lean_object* l_List_foldlM___main___at___private_Lean_Elab_Inductive_28__removeUnused___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_36__mkInductiveDecl___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_7__getResultingType(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___main___closed__1;
|
||||
lean_object* l___private_Lean_Meta_Basic_5__forallTelescopeReducingAux___at___private_Lean_Elab_Inductive_33__replaceIndFVarsWithConsts___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Array_contains___at___private_Lean_Elab_Inductive_22__addLevel___main___spec__1(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_elabInductiveViews___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l___private_Lean_Elab_Definition_1__removeUnused___closed__1;
|
||||
uint8_t l_Lean_Expr_isFVar(lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_checkValidInductiveModifier___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_7__getResultingType___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Expr_ReplaceLevelImpl_replaceUnsafeM___main___at___private_Lean_Elab_Inductive_26__updateResultingUniverse___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_mapM___main___at___private_Lean_Elab_Inductive_30__updateParams___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_checkValidInductiveModifier___closed__2;
|
||||
extern lean_object* l_Lean_Elab_Command_mkDef___lambda__1___closed__5;
|
||||
lean_object* lean_expr_update_lambda(lean_object*, uint8_t, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_checkValidInductiveModifier___closed__8;
|
||||
lean_object* l_Lean_Elab_Command_checkValidCtorModifier___closed__7;
|
||||
lean_object* l___private_Lean_Elab_Command_9__getVarDecls(lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_12__elabHeader(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_forMAux___main___at___private_Lean_Elab_Inductive_3__checkUnsafe___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___main___closed__2;
|
||||
lean_object* l_Lean_Elab_Command_getEnv(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_TraceState_Inhabited___closed__1;
|
||||
lean_object* l_Lean_Elab_Command_checkValidInductiveModifier___closed__9;
|
||||
lean_object* l_Lean_Meta_isExprDefEq(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_mapM___main___at___private_Lean_Elab_Inductive_17__levelMVarToParamAux___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_forMAux___main___at_Lean_Elab_Command_applyAttributes___spec__1(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -338,11 +359,13 @@ lean_object* l_Lean_Meta_withNewLocalInstances___main___at___private_Lean_Elab_I
|
|||
lean_object* l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___main___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_toList___rarg(lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_22__addLevel___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_checkValidInductiveModifier___closed__1;
|
||||
lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Inductive_34__mkCtor2InferMod___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Expr_Inhabited;
|
||||
lean_object* l_Lean_Elab_Command_CtorView_inhabited___closed__1;
|
||||
lean_object* l_List_forM___main___at___private_Lean_Elab_Inductive_27__traceIndTypes___spec__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_9__checkParamsAndResultType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_checkValidInductiveModifier___closed__4;
|
||||
lean_object* l_Lean_Elab_Command_CtorView_inhabited___closed__2;
|
||||
lean_object* l_Lean_Elab_Term_mkFreshLevelMVar(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Expr_ReplaceLevelImpl_replaceUnsafeM___main___at___private_Lean_Elab_Inductive_26__updateResultingUniverse___spec__4(lean_object*, size_t, lean_object*, lean_object*);
|
||||
|
|
@ -352,8 +375,10 @@ lean_object* l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___main_
|
|||
lean_object* l_Array_forMAux___main___at___private_Lean_Elab_Inductive_2__checkNumParams___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_map___main___at___private_Lean_Elab_Inductive_35__applyInferMod___spec__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_foldlM___main___at___private_Lean_Elab_Inductive_28__removeUnused___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_checkValidCtorModifier___closed__3;
|
||||
lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Inductive_34__mkCtor2InferMod___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_37__mkAuxConstructions___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_checkValidCtorModifier___closed__5;
|
||||
lean_object* l_List_map___main___at___private_Lean_Elab_Inductive_26__updateResultingUniverse___spec__6(lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_23__collectUniversesFromCtorTypeAux___main___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_23__collectUniversesFromCtorTypeAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -361,6 +386,7 @@ lean_object* l___private_Lean_Elab_Inductive_37__mkAuxConstructions___closed__1;
|
|||
lean_object* l_Lean_Expr_inferImplicit___main(lean_object*, lean_object*, uint8_t);
|
||||
lean_object* l___private_Lean_Elab_Inductive_28__removeUnused(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Meta_resettingSynthInstanceCache___rarg___closed__1;
|
||||
lean_object* l_Lean_Elab_Command_checkValidCtorModifier(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___main___closed__6;
|
||||
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_18__levelMVarToParam(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -383,6 +409,7 @@ lean_object* l___private_Lean_Elab_Inductive_36__mkInductiveDecl(lean_object*, l
|
|||
lean_object* l___private_Lean_Elab_Term_2__fromMetaException(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_mapM___main___at___private_Lean_Elab_Inductive_16__elabCtors___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_20__tmpIndParam___closed__1;
|
||||
lean_object* l_Lean_Elab_Command_checkValidInductiveModifier(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_instantiateLevelMVars(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_contains___at___private_Lean_Elab_Inductive_22__addLevel___main___spec__1___boxed(lean_object*, lean_object*);
|
||||
|
|
@ -393,6 +420,7 @@ lean_object* l_List_mapM___main___at___private_Lean_Elab_Inductive_17__levelMVar
|
|||
lean_object* l_Lean_Elab_Term_mkForall___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_33__replaceIndFVarsWithConsts___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_expr_update_const(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_checkValidCtorModifier___closed__12;
|
||||
lean_object* l___private_Lean_Elab_Inductive_19__getResultingUniverse___closed__5;
|
||||
lean_object* l_List_mapM___main___at___private_Lean_Elab_Inductive_16__elabCtors___spec__1___lambda__1___closed__5;
|
||||
lean_object* l_Lean_Meta_forallTelescopeReducing___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -412,6 +440,643 @@ lean_object* l_monadInhabited___rarg(lean_object*, lean_object*);
|
|||
lean_object* l_Lean_Meta_getFVarLocalDecl(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_forMAux___main___at___private_Lean_Elab_Inductive_37__mkAuxConstructions___spec__2(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Inductive_3__checkUnsafe(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* _init_l_Lean_Elab_Command_checkValidInductiveModifier___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("invalid use of attributes in inductive declaration");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_checkValidInductiveModifier___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Elab_Command_checkValidInductiveModifier___closed__1;
|
||||
x_2 = lean_alloc_ctor(2, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_checkValidInductiveModifier___closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Elab_Command_checkValidInductiveModifier___closed__2;
|
||||
x_2 = lean_alloc_ctor(0, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_checkValidInductiveModifier___closed__4() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("invalid use of 'partial' in inductive declaration");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_checkValidInductiveModifier___closed__5() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Elab_Command_checkValidInductiveModifier___closed__4;
|
||||
x_2 = lean_alloc_ctor(2, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_checkValidInductiveModifier___closed__6() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Elab_Command_checkValidInductiveModifier___closed__5;
|
||||
x_2 = lean_alloc_ctor(0, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_checkValidInductiveModifier___closed__7() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("invalid use of 'noncomputable' in inductive declaration");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_checkValidInductiveModifier___closed__8() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Elab_Command_checkValidInductiveModifier___closed__7;
|
||||
x_2 = lean_alloc_ctor(2, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_checkValidInductiveModifier___closed__9() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Elab_Command_checkValidInductiveModifier___closed__8;
|
||||
x_2 = lean_alloc_ctor(0, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Elab_Command_checkValidInductiveModifier(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_5; uint8_t x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10; uint8_t x_11;
|
||||
x_5 = lean_ctor_get_uint8(x_2, sizeof(void*)*2 + 1);
|
||||
x_6 = lean_ctor_get_uint8(x_2, sizeof(void*)*2 + 2);
|
||||
x_7 = lean_ctor_get(x_2, 1);
|
||||
x_8 = lean_array_get_size(x_7);
|
||||
x_9 = lean_unsigned_to_nat(0u);
|
||||
x_10 = lean_nat_dec_eq(x_8, x_9);
|
||||
if (x_5 == 0)
|
||||
{
|
||||
uint8_t x_53;
|
||||
x_53 = 0;
|
||||
x_11 = x_53;
|
||||
goto block_52;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_54;
|
||||
x_54 = 1;
|
||||
x_11 = x_54;
|
||||
goto block_52;
|
||||
}
|
||||
block_52:
|
||||
{
|
||||
uint8_t x_12;
|
||||
if (x_6 == 0)
|
||||
{
|
||||
uint8_t x_50;
|
||||
x_50 = 0;
|
||||
x_12 = x_50;
|
||||
goto block_49;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_51;
|
||||
x_51 = 1;
|
||||
x_12 = x_51;
|
||||
goto block_49;
|
||||
}
|
||||
block_49:
|
||||
{
|
||||
uint8_t x_13;
|
||||
if (x_10 == 0)
|
||||
{
|
||||
lean_object* x_41; uint8_t x_42;
|
||||
x_41 = lean_unsigned_to_nat(1u);
|
||||
x_42 = lean_nat_dec_eq(x_8, x_41);
|
||||
lean_dec(x_8);
|
||||
if (x_42 == 0)
|
||||
{
|
||||
x_13 = x_10;
|
||||
goto block_40;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; uint8_t x_47;
|
||||
x_43 = l_Lean_Elab_Command_Attribute_inhabited;
|
||||
x_44 = lean_array_get(x_43, x_7, x_9);
|
||||
x_45 = lean_ctor_get(x_44, 0);
|
||||
lean_inc(x_45);
|
||||
lean_dec(x_44);
|
||||
x_46 = l_Lean_registerClassAttr___closed__2;
|
||||
x_47 = lean_name_eq(x_45, x_46);
|
||||
lean_dec(x_45);
|
||||
x_13 = x_47;
|
||||
goto block_40;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_48;
|
||||
lean_dec(x_8);
|
||||
x_48 = 1;
|
||||
x_13 = x_48;
|
||||
goto block_40;
|
||||
}
|
||||
block_40:
|
||||
{
|
||||
uint8_t x_14;
|
||||
if (x_13 == 0)
|
||||
{
|
||||
uint8_t x_38;
|
||||
x_38 = 0;
|
||||
x_14 = x_38;
|
||||
goto block_37;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_39;
|
||||
x_39 = 1;
|
||||
x_14 = x_39;
|
||||
goto block_37;
|
||||
}
|
||||
block_37:
|
||||
{
|
||||
lean_object* x_15;
|
||||
if (x_11 == 0)
|
||||
{
|
||||
x_15 = x_4;
|
||||
goto block_30;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_31; lean_object* x_32; uint8_t x_33;
|
||||
x_31 = l_Lean_Elab_Command_checkValidInductiveModifier___closed__9;
|
||||
x_32 = l_Lean_Elab_Command_throwError___rarg(x_1, x_31, x_3, x_4);
|
||||
x_33 = !lean_is_exclusive(x_32);
|
||||
if (x_33 == 0)
|
||||
{
|
||||
return x_32;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_34; lean_object* x_35; lean_object* x_36;
|
||||
x_34 = lean_ctor_get(x_32, 0);
|
||||
x_35 = lean_ctor_get(x_32, 1);
|
||||
lean_inc(x_35);
|
||||
lean_inc(x_34);
|
||||
lean_dec(x_32);
|
||||
x_36 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_36, 0, x_34);
|
||||
lean_ctor_set(x_36, 1, x_35);
|
||||
return x_36;
|
||||
}
|
||||
}
|
||||
block_30:
|
||||
{
|
||||
if (x_12 == 0)
|
||||
{
|
||||
if (x_14 == 0)
|
||||
{
|
||||
lean_object* x_16; lean_object* x_17; uint8_t x_18;
|
||||
x_16 = l_Lean_Elab_Command_checkValidInductiveModifier___closed__3;
|
||||
x_17 = l_Lean_Elab_Command_throwError___rarg(x_1, x_16, x_3, x_15);
|
||||
x_18 = !lean_is_exclusive(x_17);
|
||||
if (x_18 == 0)
|
||||
{
|
||||
return x_17;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_19; lean_object* x_20; lean_object* x_21;
|
||||
x_19 = lean_ctor_get(x_17, 0);
|
||||
x_20 = lean_ctor_get(x_17, 1);
|
||||
lean_inc(x_20);
|
||||
lean_inc(x_19);
|
||||
lean_dec(x_17);
|
||||
x_21 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_21, 0, x_19);
|
||||
lean_ctor_set(x_21, 1, x_20);
|
||||
return x_21;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_22; lean_object* x_23;
|
||||
lean_dec(x_3);
|
||||
x_22 = lean_box(0);
|
||||
x_23 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_23, 0, x_22);
|
||||
lean_ctor_set(x_23, 1, x_15);
|
||||
return x_23;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_24; lean_object* x_25; uint8_t x_26;
|
||||
x_24 = l_Lean_Elab_Command_checkValidInductiveModifier___closed__6;
|
||||
x_25 = l_Lean_Elab_Command_throwError___rarg(x_1, x_24, x_3, x_15);
|
||||
x_26 = !lean_is_exclusive(x_25);
|
||||
if (x_26 == 0)
|
||||
{
|
||||
return x_25;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_27; lean_object* x_28; lean_object* x_29;
|
||||
x_27 = lean_ctor_get(x_25, 0);
|
||||
x_28 = lean_ctor_get(x_25, 1);
|
||||
lean_inc(x_28);
|
||||
lean_inc(x_27);
|
||||
lean_dec(x_25);
|
||||
x_29 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_29, 0, x_27);
|
||||
lean_ctor_set(x_29, 1, x_28);
|
||||
return x_29;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Elab_Command_checkValidInductiveModifier___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = l_Lean_Elab_Command_checkValidInductiveModifier(x_1, x_2, x_3, x_4);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_checkValidCtorModifier___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("invalid use of attributes in constructor declaration");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_checkValidCtorModifier___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Elab_Command_checkValidCtorModifier___closed__1;
|
||||
x_2 = lean_alloc_ctor(2, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_checkValidCtorModifier___closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Elab_Command_checkValidCtorModifier___closed__2;
|
||||
x_2 = lean_alloc_ctor(0, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_checkValidCtorModifier___closed__4() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("invalid use of 'unsafe' in constructor declaration");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_checkValidCtorModifier___closed__5() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Elab_Command_checkValidCtorModifier___closed__4;
|
||||
x_2 = lean_alloc_ctor(2, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_checkValidCtorModifier___closed__6() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Elab_Command_checkValidCtorModifier___closed__5;
|
||||
x_2 = lean_alloc_ctor(0, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_checkValidCtorModifier___closed__7() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("invalid use of 'partial' in constructor declaration");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_checkValidCtorModifier___closed__8() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Elab_Command_checkValidCtorModifier___closed__7;
|
||||
x_2 = lean_alloc_ctor(2, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_checkValidCtorModifier___closed__9() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Elab_Command_checkValidCtorModifier___closed__8;
|
||||
x_2 = lean_alloc_ctor(0, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_checkValidCtorModifier___closed__10() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("invalid use of 'noncomputable' in constructor declaration");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_checkValidCtorModifier___closed__11() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Elab_Command_checkValidCtorModifier___closed__10;
|
||||
x_2 = lean_alloc_ctor(2, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_checkValidCtorModifier___closed__12() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Elab_Command_checkValidCtorModifier___closed__11;
|
||||
x_2 = lean_alloc_ctor(0, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Elab_Command_checkValidCtorModifier(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_5; uint8_t x_6; uint8_t x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; uint8_t x_12;
|
||||
x_5 = lean_ctor_get_uint8(x_2, sizeof(void*)*2 + 1);
|
||||
x_6 = lean_ctor_get_uint8(x_2, sizeof(void*)*2 + 2);
|
||||
x_7 = lean_ctor_get_uint8(x_2, sizeof(void*)*2 + 3);
|
||||
x_8 = lean_ctor_get(x_2, 1);
|
||||
x_9 = lean_array_get_size(x_8);
|
||||
x_10 = lean_unsigned_to_nat(0u);
|
||||
x_11 = lean_nat_dec_eq(x_9, x_10);
|
||||
lean_dec(x_9);
|
||||
if (x_5 == 0)
|
||||
{
|
||||
uint8_t x_58;
|
||||
x_58 = 0;
|
||||
x_12 = x_58;
|
||||
goto block_57;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_59;
|
||||
x_59 = 1;
|
||||
x_12 = x_59;
|
||||
goto block_57;
|
||||
}
|
||||
block_57:
|
||||
{
|
||||
uint8_t x_13;
|
||||
if (x_6 == 0)
|
||||
{
|
||||
uint8_t x_55;
|
||||
x_55 = 0;
|
||||
x_13 = x_55;
|
||||
goto block_54;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_56;
|
||||
x_56 = 1;
|
||||
x_13 = x_56;
|
||||
goto block_54;
|
||||
}
|
||||
block_54:
|
||||
{
|
||||
uint8_t x_14;
|
||||
if (x_7 == 0)
|
||||
{
|
||||
uint8_t x_52;
|
||||
x_52 = 0;
|
||||
x_14 = x_52;
|
||||
goto block_51;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_53;
|
||||
x_53 = 1;
|
||||
x_14 = x_53;
|
||||
goto block_51;
|
||||
}
|
||||
block_51:
|
||||
{
|
||||
uint8_t x_15;
|
||||
if (x_11 == 0)
|
||||
{
|
||||
uint8_t x_49;
|
||||
x_49 = 1;
|
||||
x_15 = x_49;
|
||||
goto block_48;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_50;
|
||||
x_50 = 0;
|
||||
x_15 = x_50;
|
||||
goto block_48;
|
||||
}
|
||||
block_48:
|
||||
{
|
||||
uint8_t x_16;
|
||||
if (x_15 == 0)
|
||||
{
|
||||
uint8_t x_46;
|
||||
x_46 = 0;
|
||||
x_16 = x_46;
|
||||
goto block_45;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_47;
|
||||
x_47 = 1;
|
||||
x_16 = x_47;
|
||||
goto block_45;
|
||||
}
|
||||
block_45:
|
||||
{
|
||||
lean_object* x_17;
|
||||
if (x_12 == 0)
|
||||
{
|
||||
if (x_13 == 0)
|
||||
{
|
||||
x_17 = x_4;
|
||||
goto block_32;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_33; lean_object* x_34; uint8_t x_35;
|
||||
x_33 = l_Lean_Elab_Command_checkValidCtorModifier___closed__9;
|
||||
x_34 = l_Lean_Elab_Command_throwError___rarg(x_1, x_33, x_3, x_4);
|
||||
x_35 = !lean_is_exclusive(x_34);
|
||||
if (x_35 == 0)
|
||||
{
|
||||
return x_34;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_36; lean_object* x_37; lean_object* x_38;
|
||||
x_36 = lean_ctor_get(x_34, 0);
|
||||
x_37 = lean_ctor_get(x_34, 1);
|
||||
lean_inc(x_37);
|
||||
lean_inc(x_36);
|
||||
lean_dec(x_34);
|
||||
x_38 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_38, 0, x_36);
|
||||
lean_ctor_set(x_38, 1, x_37);
|
||||
return x_38;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_39; lean_object* x_40; uint8_t x_41;
|
||||
x_39 = l_Lean_Elab_Command_checkValidCtorModifier___closed__12;
|
||||
x_40 = l_Lean_Elab_Command_throwError___rarg(x_1, x_39, x_3, x_4);
|
||||
x_41 = !lean_is_exclusive(x_40);
|
||||
if (x_41 == 0)
|
||||
{
|
||||
return x_40;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_42; lean_object* x_43; lean_object* x_44;
|
||||
x_42 = lean_ctor_get(x_40, 0);
|
||||
x_43 = lean_ctor_get(x_40, 1);
|
||||
lean_inc(x_43);
|
||||
lean_inc(x_42);
|
||||
lean_dec(x_40);
|
||||
x_44 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_44, 0, x_42);
|
||||
lean_ctor_set(x_44, 1, x_43);
|
||||
return x_44;
|
||||
}
|
||||
}
|
||||
block_32:
|
||||
{
|
||||
if (x_14 == 0)
|
||||
{
|
||||
if (x_16 == 0)
|
||||
{
|
||||
lean_object* x_18; lean_object* x_19;
|
||||
lean_dec(x_3);
|
||||
x_18 = lean_box(0);
|
||||
x_19 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_19, 0, x_18);
|
||||
lean_ctor_set(x_19, 1, x_17);
|
||||
return x_19;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_20; lean_object* x_21; uint8_t x_22;
|
||||
x_20 = l_Lean_Elab_Command_checkValidCtorModifier___closed__3;
|
||||
x_21 = l_Lean_Elab_Command_throwError___rarg(x_1, x_20, x_3, x_17);
|
||||
x_22 = !lean_is_exclusive(x_21);
|
||||
if (x_22 == 0)
|
||||
{
|
||||
return x_21;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_23; lean_object* x_24; lean_object* x_25;
|
||||
x_23 = lean_ctor_get(x_21, 0);
|
||||
x_24 = lean_ctor_get(x_21, 1);
|
||||
lean_inc(x_24);
|
||||
lean_inc(x_23);
|
||||
lean_dec(x_21);
|
||||
x_25 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_25, 0, x_23);
|
||||
lean_ctor_set(x_25, 1, x_24);
|
||||
return x_25;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_26; lean_object* x_27; uint8_t x_28;
|
||||
x_26 = l_Lean_Elab_Command_checkValidCtorModifier___closed__6;
|
||||
x_27 = l_Lean_Elab_Command_throwError___rarg(x_1, x_26, x_3, x_17);
|
||||
x_28 = !lean_is_exclusive(x_27);
|
||||
if (x_28 == 0)
|
||||
{
|
||||
return x_27;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_29; lean_object* x_30; lean_object* x_31;
|
||||
x_29 = lean_ctor_get(x_27, 0);
|
||||
x_30 = lean_ctor_get(x_27, 1);
|
||||
lean_inc(x_30);
|
||||
lean_inc(x_29);
|
||||
lean_dec(x_27);
|
||||
x_31 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_31, 0, x_29);
|
||||
lean_ctor_set(x_31, 1, x_30);
|
||||
return x_31;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Elab_Command_checkValidCtorModifier___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = l_Lean_Elab_Command_checkValidCtorModifier(x_1, x_2, x_3, x_4);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Elab_Command_CtorView_inhabited___closed__1() {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -19871,7 +20536,7 @@ lean_dec(x_1);
|
|||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_forMAux___main___at_Lean_Elab_Command_elabInductiveCore___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
lean_object* l_Array_forMAux___main___at_Lean_Elab_Command_elabInductiveViews___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_6; uint8_t x_7;
|
||||
|
|
@ -19946,7 +20611,7 @@ return x_24;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Elab_Command_elabInductiveCore___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
lean_object* l_Lean_Elab_Command_elabInductiveViews___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
|
|
@ -19954,7 +20619,7 @@ x_5 = l___private_Lean_Elab_Inductive_36__mkInductiveDecl(x_2, x_1, x_3, x_4);
|
|||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Elab_Command_elabInductiveCore(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
lean_object* l_Lean_Elab_Command_elabInductiveViews(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37;
|
||||
|
|
@ -19969,7 +20634,7 @@ lean_dec(x_6);
|
|||
x_35 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_35, 0, x_34);
|
||||
lean_inc(x_1);
|
||||
x_36 = lean_alloc_closure((void*)(l_Lean_Elab_Command_elabInductiveCore___lambda__1), 4, 1);
|
||||
x_36 = lean_alloc_closure((void*)(l_Lean_Elab_Command_elabInductiveViews___lambda__1), 4, 1);
|
||||
lean_closure_set(x_36, 0, x_1);
|
||||
lean_inc(x_2);
|
||||
x_37 = l___private_Lean_Elab_Command_2__getState(x_2, x_3);
|
||||
|
|
@ -20470,7 +21135,7 @@ lean_object* x_13; lean_object* x_14;
|
|||
x_13 = lean_ctor_get(x_12, 1);
|
||||
lean_inc(x_13);
|
||||
lean_dec(x_12);
|
||||
x_14 = l_Array_forMAux___main___at_Lean_Elab_Command_elabInductiveCore___spec__1(x_7, x_1, x_5, x_2, x_13);
|
||||
x_14 = l_Array_forMAux___main___at_Lean_Elab_Command_elabInductiveViews___spec__1(x_7, x_1, x_5, x_2, x_13);
|
||||
lean_dec(x_1);
|
||||
lean_dec(x_7);
|
||||
if (lean_obj_tag(x_14) == 0)
|
||||
|
|
@ -20576,11 +21241,11 @@ return x_32;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_forMAux___main___at_Lean_Elab_Command_elabInductiveCore___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
lean_object* l_Array_forMAux___main___at_Lean_Elab_Command_elabInductiveViews___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_6;
|
||||
x_6 = l_Array_forMAux___main___at_Lean_Elab_Command_elabInductiveCore___spec__1(x_1, x_2, x_3, x_4, x_5);
|
||||
x_6 = l_Array_forMAux___main___at_Lean_Elab_Command_elabInductiveViews___spec__1(x_1, x_2, x_3, x_4, x_5);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
return x_6;
|
||||
|
|
@ -20623,6 +21288,48 @@ lean_dec_ref(res);
|
|||
res = initialize_Lean_Elab_Definition(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
l_Lean_Elab_Command_checkValidInductiveModifier___closed__1 = _init_l_Lean_Elab_Command_checkValidInductiveModifier___closed__1();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_checkValidInductiveModifier___closed__1);
|
||||
l_Lean_Elab_Command_checkValidInductiveModifier___closed__2 = _init_l_Lean_Elab_Command_checkValidInductiveModifier___closed__2();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_checkValidInductiveModifier___closed__2);
|
||||
l_Lean_Elab_Command_checkValidInductiveModifier___closed__3 = _init_l_Lean_Elab_Command_checkValidInductiveModifier___closed__3();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_checkValidInductiveModifier___closed__3);
|
||||
l_Lean_Elab_Command_checkValidInductiveModifier___closed__4 = _init_l_Lean_Elab_Command_checkValidInductiveModifier___closed__4();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_checkValidInductiveModifier___closed__4);
|
||||
l_Lean_Elab_Command_checkValidInductiveModifier___closed__5 = _init_l_Lean_Elab_Command_checkValidInductiveModifier___closed__5();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_checkValidInductiveModifier___closed__5);
|
||||
l_Lean_Elab_Command_checkValidInductiveModifier___closed__6 = _init_l_Lean_Elab_Command_checkValidInductiveModifier___closed__6();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_checkValidInductiveModifier___closed__6);
|
||||
l_Lean_Elab_Command_checkValidInductiveModifier___closed__7 = _init_l_Lean_Elab_Command_checkValidInductiveModifier___closed__7();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_checkValidInductiveModifier___closed__7);
|
||||
l_Lean_Elab_Command_checkValidInductiveModifier___closed__8 = _init_l_Lean_Elab_Command_checkValidInductiveModifier___closed__8();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_checkValidInductiveModifier___closed__8);
|
||||
l_Lean_Elab_Command_checkValidInductiveModifier___closed__9 = _init_l_Lean_Elab_Command_checkValidInductiveModifier___closed__9();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_checkValidInductiveModifier___closed__9);
|
||||
l_Lean_Elab_Command_checkValidCtorModifier___closed__1 = _init_l_Lean_Elab_Command_checkValidCtorModifier___closed__1();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_checkValidCtorModifier___closed__1);
|
||||
l_Lean_Elab_Command_checkValidCtorModifier___closed__2 = _init_l_Lean_Elab_Command_checkValidCtorModifier___closed__2();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_checkValidCtorModifier___closed__2);
|
||||
l_Lean_Elab_Command_checkValidCtorModifier___closed__3 = _init_l_Lean_Elab_Command_checkValidCtorModifier___closed__3();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_checkValidCtorModifier___closed__3);
|
||||
l_Lean_Elab_Command_checkValidCtorModifier___closed__4 = _init_l_Lean_Elab_Command_checkValidCtorModifier___closed__4();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_checkValidCtorModifier___closed__4);
|
||||
l_Lean_Elab_Command_checkValidCtorModifier___closed__5 = _init_l_Lean_Elab_Command_checkValidCtorModifier___closed__5();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_checkValidCtorModifier___closed__5);
|
||||
l_Lean_Elab_Command_checkValidCtorModifier___closed__6 = _init_l_Lean_Elab_Command_checkValidCtorModifier___closed__6();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_checkValidCtorModifier___closed__6);
|
||||
l_Lean_Elab_Command_checkValidCtorModifier___closed__7 = _init_l_Lean_Elab_Command_checkValidCtorModifier___closed__7();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_checkValidCtorModifier___closed__7);
|
||||
l_Lean_Elab_Command_checkValidCtorModifier___closed__8 = _init_l_Lean_Elab_Command_checkValidCtorModifier___closed__8();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_checkValidCtorModifier___closed__8);
|
||||
l_Lean_Elab_Command_checkValidCtorModifier___closed__9 = _init_l_Lean_Elab_Command_checkValidCtorModifier___closed__9();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_checkValidCtorModifier___closed__9);
|
||||
l_Lean_Elab_Command_checkValidCtorModifier___closed__10 = _init_l_Lean_Elab_Command_checkValidCtorModifier___closed__10();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_checkValidCtorModifier___closed__10);
|
||||
l_Lean_Elab_Command_checkValidCtorModifier___closed__11 = _init_l_Lean_Elab_Command_checkValidCtorModifier___closed__11();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_checkValidCtorModifier___closed__11);
|
||||
l_Lean_Elab_Command_checkValidCtorModifier___closed__12 = _init_l_Lean_Elab_Command_checkValidCtorModifier___closed__12();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_checkValidCtorModifier___closed__12);
|
||||
l_Lean_Elab_Command_CtorView_inhabited___closed__1 = _init_l_Lean_Elab_Command_CtorView_inhabited___closed__1();
|
||||
lean_mark_persistent(l_Lean_Elab_Command_CtorView_inhabited___closed__1);
|
||||
l_Lean_Elab_Command_CtorView_inhabited___closed__2 = _init_l_Lean_Elab_Command_CtorView_inhabited___closed__2();
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
File diff suppressed because it is too large
Load diff
Loading…
Add table
Reference in a new issue