diff --git a/stage0/src/Std/Data.lean b/stage0/src/Std/Data.lean index c8a99e4082..3199055a78 100644 --- a/stage0/src/Std/Data.lean +++ b/stage0/src/Std/Data.lean @@ -3,5 +3,4 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ --- import Std.Data.BinomialHeap -def test := 10 +import Std.Data.BinomialHeap diff --git a/stage0/src/Init/Data/BinomialHeap.lean b/stage0/src/Std/Data/BinomialHeap.lean similarity index 78% rename from stage0/src/Init/Data/BinomialHeap.lean rename to stage0/src/Std/Data/BinomialHeap.lean index 48d33def3b..7444f46067 100644 --- a/stage0/src/Init/Data/BinomialHeap.lean +++ b/stage0/src/Std/Data/BinomialHeap.lean @@ -3,5 +3,4 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ -prelude -import Init.Data.BinomialHeap.Basic +import Std.Data.BinomialHeap.Basic diff --git a/stage0/src/Init/Data/BinomialHeap/Basic.lean b/stage0/src/Std/Data/BinomialHeap/Basic.lean similarity index 99% rename from stage0/src/Init/Data/BinomialHeap/Basic.lean rename to stage0/src/Std/Data/BinomialHeap/Basic.lean index a658741e23..6282e53e94 100644 --- a/stage0/src/Init/Data/BinomialHeap/Basic.lean +++ b/stage0/src/Std/Data/BinomialHeap/Basic.lean @@ -3,10 +3,10 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ -prelude import Init.Data.List -universes u +namespace Std +universes u namespace BinomialHeapImp structure HeapNodeAux (α : Type u) (h : Type u) := @@ -146,3 +146,4 @@ merge (singleton a) h | ⟨b, _⟩ => BinomialHeapImp.toList lt b end BinomialHeap +end Std diff --git a/stage0/stdlib/CMakeLists.txt b/stage0/stdlib/CMakeLists.txt index 753612a736..374f9b281a 100644 --- a/stage0/stdlib/CMakeLists.txt +++ b/stage0/stdlib/CMakeLists.txt @@ -1 +1 @@ -add_library (stage0 OBJECT ./Init.c ./Init/Coe.c ./Init/Control.c ./Init/Control/Alternative.c ./Init/Control/Applicative.c ./Init/Control/Conditional.c ./Init/Control/EState.c ./Init/Control/Except.c ./Init/Control/Functor.c ./Init/Control/Id.c ./Init/Control/Lift.c ./Init/Control/Monad.c ./Init/Control/Option.c ./Init/Control/Reader.c ./Init/Control/State.c ./Init/Core.c ./Init/Data.c ./Init/Data/Array.c ./Init/Data/Array/Basic.c ./Init/Data/Array/BinSearch.c ./Init/Data/Array/QSort.c ./Init/Data/AssocList.c ./Init/Data/Basic.c ./Init/Data/BinomialHeap.c ./Init/Data/BinomialHeap/Basic.c ./Init/Data/ByteArray.c ./Init/Data/ByteArray/Basic.c ./Init/Data/Char.c ./Init/Data/Char/Basic.c ./Init/Data/DList.c ./Init/Data/Fin.c ./Init/Data/Fin/Basic.c ./Init/Data/Float.c ./Init/Data/FloatArray.c ./Init/Data/FloatArray/Basic.c ./Init/Data/HashMap.c ./Init/Data/HashMap/Basic.c ./Init/Data/HashSet.c ./Init/Data/Hashable.c ./Init/Data/Int.c ./Init/Data/Int/Basic.c ./Init/Data/List.c ./Init/Data/List/Basic.c ./Init/Data/List/BasicAux.c ./Init/Data/List/Control.c ./Init/Data/List/Instances.c ./Init/Data/Nat.c ./Init/Data/Nat/Basic.c ./Init/Data/Nat/Bitwise.c ./Init/Data/Nat/Control.c ./Init/Data/Nat/Div.c ./Init/Data/Option.c ./Init/Data/Option/Basic.c ./Init/Data/Option/BasicAux.c ./Init/Data/Option/Instances.c ./Init/Data/PersistentArray.c ./Init/Data/PersistentArray/Basic.c ./Init/Data/PersistentHashMap.c ./Init/Data/PersistentHashMap/Basic.c ./Init/Data/PersistentHashSet.c ./Init/Data/Queue.c ./Init/Data/Queue/Basic.c ./Init/Data/RBMap.c ./Init/Data/RBMap/Basic.c ./Init/Data/RBMap/BasicAux.c ./Init/Data/RBTree.c ./Init/Data/RBTree/Basic.c ./Init/Data/Random.c ./Init/Data/Repr.c ./Init/Data/Stack.c ./Init/Data/Stack/Basic.c ./Init/Data/String.c ./Init/Data/String/Basic.c ./Init/Data/String/Extra.c ./Init/Data/ToString.c ./Init/Data/UInt.c ./Init/Fix.c ./Init/HasCoe.c ./Init/Lean.c ./Init/Lean/Attributes.c ./Init/Lean/AuxRecursor.c ./Init/Lean/Class.c ./Init/Lean/Compiler.c ./Init/Lean/Compiler/ClosedTermCache.c ./Init/Lean/Compiler/ConstFolding.c ./Init/Lean/Compiler/ExportAttr.c ./Init/Lean/Compiler/ExternAttr.c ./Init/Lean/Compiler/IR.c ./Init/Lean/Compiler/IR/Basic.c ./Init/Lean/Compiler/IR/Borrow.c ./Init/Lean/Compiler/IR/Boxing.c ./Init/Lean/Compiler/IR/Checker.c ./Init/Lean/Compiler/IR/CompilerM.c ./Init/Lean/Compiler/IR/CtorLayout.c ./Init/Lean/Compiler/IR/ElimDeadBranches.c ./Init/Lean/Compiler/IR/ElimDeadVars.c ./Init/Lean/Compiler/IR/EmitC.c ./Init/Lean/Compiler/IR/EmitUtil.c ./Init/Lean/Compiler/IR/ExpandResetReuse.c ./Init/Lean/Compiler/IR/Format.c ./Init/Lean/Compiler/IR/FreeVars.c ./Init/Lean/Compiler/IR/LiveVars.c ./Init/Lean/Compiler/IR/NormIds.c ./Init/Lean/Compiler/IR/PushProj.c ./Init/Lean/Compiler/IR/RC.c ./Init/Lean/Compiler/IR/ResetReuse.c ./Init/Lean/Compiler/IR/SimpCase.c ./Init/Lean/Compiler/IR/UnboxResult.c ./Init/Lean/Compiler/ImplementedByAttr.c ./Init/Lean/Compiler/InitAttr.c ./Init/Lean/Compiler/InlineAttrs.c ./Init/Lean/Compiler/NameMangling.c ./Init/Lean/Compiler/NeverExtractAttr.c ./Init/Lean/Compiler/Specialize.c ./Init/Lean/Compiler/Util.c ./Init/Lean/Data/Format.c ./Init/Lean/Data/Json.c ./Init/Lean/Data/Json/Basic.c ./Init/Lean/Data/Json/FromToJson.c ./Init/Lean/Data/Json/Parser.c ./Init/Lean/Data/Json/Printer.c ./Init/Lean/Data/KVMap.c ./Init/Lean/Data/LBool.c ./Init/Lean/Data/LOption.c ./Init/Lean/Data/Name.c ./Init/Lean/Data/Occurrences.c ./Init/Lean/Data/Options.c ./Init/Lean/Data/Position.c ./Init/Lean/Data/SMap.c ./Init/Lean/Data/Trie.c ./Init/Lean/Declaration.c ./Init/Lean/Delaborator.c ./Init/Lean/Elab.c ./Init/Lean/Elab/Alias.c ./Init/Lean/Elab/App.c ./Init/Lean/Elab/Binders.c ./Init/Lean/Elab/BuiltinNotation.c ./Init/Lean/Elab/Command.c ./Init/Lean/Elab/DeclModifiers.c ./Init/Lean/Elab/Declaration.c ./Init/Lean/Elab/Definition.c ./Init/Lean/Elab/DoNotation.c ./Init/Lean/Elab/Exception.c ./Init/Lean/Elab/Frontend.c ./Init/Lean/Elab/Import.c ./Init/Lean/Elab/Level.c ./Init/Lean/Elab/Log.c ./Init/Lean/Elab/Match.c ./Init/Lean/Elab/Quotation.c ./Init/Lean/Elab/ResolveName.c ./Init/Lean/Elab/StrategyAttrs.c ./Init/Lean/Elab/StructInst.c ./Init/Lean/Elab/Syntax.c ./Init/Lean/Elab/SyntheticMVars.c ./Init/Lean/Elab/Tactic.c ./Init/Lean/Elab/Tactic/Basic.c ./Init/Lean/Elab/Tactic/ElabTerm.c ./Init/Lean/Elab/Tactic/Generalize.c ./Init/Lean/Elab/Tactic/Induction.c ./Init/Lean/Elab/Tactic/Injection.c ./Init/Lean/Elab/Term.c ./Init/Lean/Elab/Util.c ./Init/Lean/Environment.c ./Init/Lean/EqnCompiler.c ./Init/Lean/EqnCompiler/MatchPattern.c ./Init/Lean/Eval.c ./Init/Lean/Expr.c ./Init/Lean/HeadIndex.c ./Init/Lean/Hygiene.c ./Init/Lean/KeyedDeclsAttribute.c ./Init/Lean/Level.c ./Init/Lean/Linter.c ./Init/Lean/LocalContext.c ./Init/Lean/Message.c ./Init/Lean/Meta.c ./Init/Lean/Meta/AbstractMVars.c ./Init/Lean/Meta/AppBuilder.c ./Init/Lean/Meta/Basic.c ./Init/Lean/Meta/Check.c ./Init/Lean/Meta/DiscrTree.c ./Init/Lean/Meta/DiscrTreeTypes.c ./Init/Lean/Meta/Exception.c ./Init/Lean/Meta/ExprDefEq.c ./Init/Lean/Meta/FunInfo.c ./Init/Lean/Meta/GeneralizeTelescope.c ./Init/Lean/Meta/InferType.c ./Init/Lean/Meta/Instances.c ./Init/Lean/Meta/KAbstract.c ./Init/Lean/Meta/LevelDefEq.c ./Init/Lean/Meta/Message.c ./Init/Lean/Meta/Offset.c ./Init/Lean/Meta/RecursorInfo.c ./Init/Lean/Meta/Reduce.c ./Init/Lean/Meta/SynthInstance.c ./Init/Lean/Meta/Tactic.c ./Init/Lean/Meta/Tactic/Apply.c ./Init/Lean/Meta/Tactic/Assert.c ./Init/Lean/Meta/Tactic/Assumption.c ./Init/Lean/Meta/Tactic/Cases.c ./Init/Lean/Meta/Tactic/Clear.c ./Init/Lean/Meta/Tactic/FVarSubst.c ./Init/Lean/Meta/Tactic/Generalize.c ./Init/Lean/Meta/Tactic/Induction.c ./Init/Lean/Meta/Tactic/Injection.c ./Init/Lean/Meta/Tactic/Intro.c ./Init/Lean/Meta/Tactic/LocalDecl.c ./Init/Lean/Meta/Tactic/Revert.c ./Init/Lean/Meta/Tactic/Rewrite.c ./Init/Lean/Meta/Tactic/Subst.c ./Init/Lean/Meta/Tactic/Target.c ./Init/Lean/Meta/Tactic/Util.c ./Init/Lean/Meta/WHNF.c ./Init/Lean/MetavarContext.c ./Init/Lean/Modifiers.c ./Init/Lean/Parser.c ./Init/Lean/Parser/Command.c ./Init/Lean/Parser/Level.c ./Init/Lean/Parser/Module.c ./Init/Lean/Parser/Parser.c ./Init/Lean/Parser/Syntax.c ./Init/Lean/Parser/Tactic.c ./Init/Lean/Parser/Term.c ./Init/Lean/Parser/Transform.c ./Init/Lean/PrettyPrinter.c ./Init/Lean/PrettyPrinter/Parenthesizer.c ./Init/Lean/ProjFns.c ./Init/Lean/ReducibilityAttrs.c ./Init/Lean/Runtime.c ./Init/Lean/Scopes.c ./Init/Lean/Structure.c ./Init/Lean/Syntax.c ./Init/Lean/ToExpr.c ./Init/Lean/Util.c ./Init/Lean/Util/Closure.c ./Init/Lean/Util/CollectFVars.c ./Init/Lean/Util/CollectLevelParams.c ./Init/Lean/Util/CollectMVars.c ./Init/Lean/Util/FindExpr.c ./Init/Lean/Util/FindMVar.c ./Init/Lean/Util/FoldConsts.c ./Init/Lean/Util/MonadCache.c ./Init/Lean/Util/PPExt.c ./Init/Lean/Util/PPGoal.c ./Init/Lean/Util/Path.c ./Init/Lean/Util/Profile.c ./Init/Lean/Util/RecDepth.c ./Init/Lean/Util/Recognizers.c ./Init/Lean/Util/ReplaceExpr.c ./Init/Lean/Util/Sorry.c ./Init/Lean/Util/Trace.c ./Init/Lean/Util/WHNF.c ./Init/LeanInit.c ./Init/ShareCommon.c ./Init/System.c ./Init/System/FilePath.c ./Init/System/IO.c ./Init/System/IOError.c ./Init/System/Platform.c ./Init/Util.c ./Init/WF.c ./Std/Data.c ) +add_library (stage0 OBJECT ./Init.c ./Init/Coe.c ./Init/Control.c ./Init/Control/Alternative.c ./Init/Control/Applicative.c ./Init/Control/Conditional.c ./Init/Control/EState.c ./Init/Control/Except.c ./Init/Control/Functor.c ./Init/Control/Id.c ./Init/Control/Lift.c ./Init/Control/Monad.c ./Init/Control/Option.c ./Init/Control/Reader.c ./Init/Control/State.c ./Init/Core.c ./Init/Data.c ./Init/Data/Array.c ./Init/Data/Array/Basic.c ./Init/Data/Array/BinSearch.c ./Init/Data/Array/QSort.c ./Init/Data/AssocList.c ./Init/Data/Basic.c ./Init/Data/ByteArray.c ./Init/Data/ByteArray/Basic.c ./Init/Data/Char.c ./Init/Data/Char/Basic.c ./Init/Data/DList.c ./Init/Data/Fin.c ./Init/Data/Fin/Basic.c ./Init/Data/Float.c ./Init/Data/FloatArray.c ./Init/Data/FloatArray/Basic.c ./Init/Data/HashMap.c ./Init/Data/HashMap/Basic.c ./Init/Data/HashSet.c ./Init/Data/Hashable.c ./Init/Data/Int.c ./Init/Data/Int/Basic.c ./Init/Data/List.c ./Init/Data/List/Basic.c ./Init/Data/List/BasicAux.c ./Init/Data/List/Control.c ./Init/Data/List/Instances.c ./Init/Data/Nat.c ./Init/Data/Nat/Basic.c ./Init/Data/Nat/Bitwise.c ./Init/Data/Nat/Control.c ./Init/Data/Nat/Div.c ./Init/Data/Option.c ./Init/Data/Option/Basic.c ./Init/Data/Option/BasicAux.c ./Init/Data/Option/Instances.c ./Init/Data/PersistentArray.c ./Init/Data/PersistentArray/Basic.c ./Init/Data/PersistentHashMap.c ./Init/Data/PersistentHashMap/Basic.c ./Init/Data/PersistentHashSet.c ./Init/Data/Queue.c ./Init/Data/Queue/Basic.c ./Init/Data/RBMap.c ./Init/Data/RBMap/Basic.c ./Init/Data/RBMap/BasicAux.c ./Init/Data/RBTree.c ./Init/Data/RBTree/Basic.c ./Init/Data/Random.c ./Init/Data/Repr.c ./Init/Data/Stack.c ./Init/Data/Stack/Basic.c ./Init/Data/String.c ./Init/Data/String/Basic.c ./Init/Data/String/Extra.c ./Init/Data/ToString.c ./Init/Data/UInt.c ./Init/Fix.c ./Init/HasCoe.c ./Init/Lean.c ./Init/Lean/Attributes.c ./Init/Lean/AuxRecursor.c ./Init/Lean/Class.c ./Init/Lean/Compiler.c ./Init/Lean/Compiler/ClosedTermCache.c ./Init/Lean/Compiler/ConstFolding.c ./Init/Lean/Compiler/ExportAttr.c ./Init/Lean/Compiler/ExternAttr.c ./Init/Lean/Compiler/IR.c ./Init/Lean/Compiler/IR/Basic.c ./Init/Lean/Compiler/IR/Borrow.c ./Init/Lean/Compiler/IR/Boxing.c ./Init/Lean/Compiler/IR/Checker.c ./Init/Lean/Compiler/IR/CompilerM.c ./Init/Lean/Compiler/IR/CtorLayout.c ./Init/Lean/Compiler/IR/ElimDeadBranches.c ./Init/Lean/Compiler/IR/ElimDeadVars.c ./Init/Lean/Compiler/IR/EmitC.c ./Init/Lean/Compiler/IR/EmitUtil.c ./Init/Lean/Compiler/IR/ExpandResetReuse.c ./Init/Lean/Compiler/IR/Format.c ./Init/Lean/Compiler/IR/FreeVars.c ./Init/Lean/Compiler/IR/LiveVars.c ./Init/Lean/Compiler/IR/NormIds.c ./Init/Lean/Compiler/IR/PushProj.c ./Init/Lean/Compiler/IR/RC.c ./Init/Lean/Compiler/IR/ResetReuse.c ./Init/Lean/Compiler/IR/SimpCase.c ./Init/Lean/Compiler/IR/UnboxResult.c ./Init/Lean/Compiler/ImplementedByAttr.c ./Init/Lean/Compiler/InitAttr.c ./Init/Lean/Compiler/InlineAttrs.c ./Init/Lean/Compiler/NameMangling.c ./Init/Lean/Compiler/NeverExtractAttr.c ./Init/Lean/Compiler/Specialize.c ./Init/Lean/Compiler/Util.c ./Init/Lean/Data/Format.c ./Init/Lean/Data/Json.c ./Init/Lean/Data/Json/Basic.c ./Init/Lean/Data/Json/FromToJson.c ./Init/Lean/Data/Json/Parser.c ./Init/Lean/Data/Json/Printer.c ./Init/Lean/Data/KVMap.c ./Init/Lean/Data/LBool.c ./Init/Lean/Data/LOption.c ./Init/Lean/Data/Name.c ./Init/Lean/Data/Occurrences.c ./Init/Lean/Data/Options.c ./Init/Lean/Data/Position.c ./Init/Lean/Data/SMap.c ./Init/Lean/Data/Trie.c ./Init/Lean/Declaration.c ./Init/Lean/Delaborator.c ./Init/Lean/Elab.c ./Init/Lean/Elab/Alias.c ./Init/Lean/Elab/App.c ./Init/Lean/Elab/Binders.c ./Init/Lean/Elab/BuiltinNotation.c ./Init/Lean/Elab/Command.c ./Init/Lean/Elab/DeclModifiers.c ./Init/Lean/Elab/Declaration.c ./Init/Lean/Elab/Definition.c ./Init/Lean/Elab/DoNotation.c ./Init/Lean/Elab/Exception.c ./Init/Lean/Elab/Frontend.c ./Init/Lean/Elab/Import.c ./Init/Lean/Elab/Level.c ./Init/Lean/Elab/Log.c ./Init/Lean/Elab/Match.c ./Init/Lean/Elab/Quotation.c ./Init/Lean/Elab/ResolveName.c ./Init/Lean/Elab/StrategyAttrs.c ./Init/Lean/Elab/StructInst.c ./Init/Lean/Elab/Syntax.c ./Init/Lean/Elab/SyntheticMVars.c ./Init/Lean/Elab/Tactic.c ./Init/Lean/Elab/Tactic/Basic.c ./Init/Lean/Elab/Tactic/ElabTerm.c ./Init/Lean/Elab/Tactic/Generalize.c ./Init/Lean/Elab/Tactic/Induction.c ./Init/Lean/Elab/Tactic/Injection.c ./Init/Lean/Elab/Term.c ./Init/Lean/Elab/Util.c ./Init/Lean/Environment.c ./Init/Lean/EqnCompiler.c ./Init/Lean/EqnCompiler/MatchPattern.c ./Init/Lean/Eval.c ./Init/Lean/Expr.c ./Init/Lean/HeadIndex.c ./Init/Lean/Hygiene.c ./Init/Lean/KeyedDeclsAttribute.c ./Init/Lean/Level.c ./Init/Lean/Linter.c ./Init/Lean/LocalContext.c ./Init/Lean/Message.c ./Init/Lean/Meta.c ./Init/Lean/Meta/AbstractMVars.c ./Init/Lean/Meta/AppBuilder.c ./Init/Lean/Meta/Basic.c ./Init/Lean/Meta/Check.c ./Init/Lean/Meta/DiscrTree.c ./Init/Lean/Meta/DiscrTreeTypes.c ./Init/Lean/Meta/Exception.c ./Init/Lean/Meta/ExprDefEq.c ./Init/Lean/Meta/FunInfo.c ./Init/Lean/Meta/GeneralizeTelescope.c ./Init/Lean/Meta/InferType.c ./Init/Lean/Meta/Instances.c ./Init/Lean/Meta/KAbstract.c ./Init/Lean/Meta/LevelDefEq.c ./Init/Lean/Meta/Message.c ./Init/Lean/Meta/Offset.c ./Init/Lean/Meta/RecursorInfo.c ./Init/Lean/Meta/Reduce.c ./Init/Lean/Meta/SynthInstance.c ./Init/Lean/Meta/Tactic.c ./Init/Lean/Meta/Tactic/Apply.c ./Init/Lean/Meta/Tactic/Assert.c ./Init/Lean/Meta/Tactic/Assumption.c ./Init/Lean/Meta/Tactic/Cases.c ./Init/Lean/Meta/Tactic/Clear.c ./Init/Lean/Meta/Tactic/FVarSubst.c ./Init/Lean/Meta/Tactic/Generalize.c ./Init/Lean/Meta/Tactic/Induction.c ./Init/Lean/Meta/Tactic/Injection.c ./Init/Lean/Meta/Tactic/Intro.c ./Init/Lean/Meta/Tactic/LocalDecl.c ./Init/Lean/Meta/Tactic/Revert.c ./Init/Lean/Meta/Tactic/Rewrite.c ./Init/Lean/Meta/Tactic/Subst.c ./Init/Lean/Meta/Tactic/Target.c ./Init/Lean/Meta/Tactic/Util.c ./Init/Lean/Meta/WHNF.c ./Init/Lean/MetavarContext.c ./Init/Lean/Modifiers.c ./Init/Lean/Parser.c ./Init/Lean/Parser/Command.c ./Init/Lean/Parser/Level.c ./Init/Lean/Parser/Module.c ./Init/Lean/Parser/Parser.c ./Init/Lean/Parser/Syntax.c ./Init/Lean/Parser/Tactic.c ./Init/Lean/Parser/Term.c ./Init/Lean/Parser/Transform.c ./Init/Lean/PrettyPrinter.c ./Init/Lean/PrettyPrinter/Parenthesizer.c ./Init/Lean/ProjFns.c ./Init/Lean/ReducibilityAttrs.c ./Init/Lean/Runtime.c ./Init/Lean/Scopes.c ./Init/Lean/Structure.c ./Init/Lean/Syntax.c ./Init/Lean/ToExpr.c ./Init/Lean/Util.c ./Init/Lean/Util/Closure.c ./Init/Lean/Util/CollectFVars.c ./Init/Lean/Util/CollectLevelParams.c ./Init/Lean/Util/CollectMVars.c ./Init/Lean/Util/FindExpr.c ./Init/Lean/Util/FindMVar.c ./Init/Lean/Util/FoldConsts.c ./Init/Lean/Util/MonadCache.c ./Init/Lean/Util/PPExt.c ./Init/Lean/Util/PPGoal.c ./Init/Lean/Util/Path.c ./Init/Lean/Util/Profile.c ./Init/Lean/Util/RecDepth.c ./Init/Lean/Util/Recognizers.c ./Init/Lean/Util/ReplaceExpr.c ./Init/Lean/Util/Sorry.c ./Init/Lean/Util/Trace.c ./Init/Lean/Util/WHNF.c ./Init/LeanInit.c ./Init/ShareCommon.c ./Init/System.c ./Init/System/FilePath.c ./Init/System/IO.c ./Init/System/IOError.c ./Init/System/Platform.c ./Init/Util.c ./Init/WF.c ./Std/Data.c ./Std/Data/BinomialHeap.c ./Std/Data/BinomialHeap/Basic.c ) diff --git a/stage0/stdlib/Std/Data.c b/stage0/stdlib/Std/Data.c index 9cd3c0e8cd..66f09c9d71 100644 --- a/stage0/stdlib/Std/Data.c +++ b/stage0/stdlib/Std/Data.c @@ -1,6 +1,6 @@ // Lean compiler output // Module: Std.Data -// Imports: Init +// Imports: Init Std.Data.BinomialHeap #include #if defined(__clang__) #pragma clang diagnostic ignored "-Wunused-parameter" @@ -13,16 +13,8 @@ #ifdef __cplusplus extern "C" { #endif -lean_object* l_test; -lean_object* _init_l_test() { -_start: -{ -lean_object* x_1; -x_1 = lean_unsigned_to_nat(10u); -return x_1; -} -} lean_object* initialize_Init(lean_object*); +lean_object* initialize_Std_Data_BinomialHeap(lean_object*); static bool _G_initialized = false; lean_object* initialize_Std_Data(lean_object* w) { lean_object * res; @@ -31,8 +23,9 @@ _G_initialized = true; res = initialize_Init(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); -l_test = _init_l_test(); -lean_mark_persistent(l_test); +res = initialize_Std_Data_BinomialHeap(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 diff --git a/stage0/stdlib/Init/Data/BinomialHeap.c b/stage0/stdlib/Std/Data/BinomialHeap.c similarity index 62% rename from stage0/stdlib/Init/Data/BinomialHeap.c rename to stage0/stdlib/Std/Data/BinomialHeap.c index 2ed28b3e02..ecc727267a 100644 --- a/stage0/stdlib/Init/Data/BinomialHeap.c +++ b/stage0/stdlib/Std/Data/BinomialHeap.c @@ -1,6 +1,6 @@ // Lean compiler output -// Module: Init.Data.BinomialHeap -// Imports: Init.Data.BinomialHeap.Basic +// Module: Std.Data.BinomialHeap +// Imports: Init Std.Data.BinomialHeap.Basic #include #if defined(__clang__) #pragma clang diagnostic ignored "-Wunused-parameter" @@ -13,13 +13,17 @@ #ifdef __cplusplus extern "C" { #endif -lean_object* initialize_Init_Data_BinomialHeap_Basic(lean_object*); +lean_object* initialize_Init(lean_object*); +lean_object* initialize_Std_Data_BinomialHeap_Basic(lean_object*); static bool _G_initialized = false; -lean_object* initialize_Init_Data_BinomialHeap(lean_object* w) { +lean_object* initialize_Std_Data_BinomialHeap(lean_object* w) { lean_object * res; if (_G_initialized) return lean_mk_io_result(lean_box(0)); _G_initialized = true; -res = initialize_Init_Data_BinomialHeap_Basic(lean_io_mk_world()); +res = initialize_Init(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +res = initialize_Std_Data_BinomialHeap_Basic(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)); diff --git a/stage0/stdlib/Init/Data/BinomialHeap/Basic.c b/stage0/stdlib/Std/Data/BinomialHeap/Basic.c similarity index 59% rename from stage0/stdlib/Init/Data/BinomialHeap/Basic.c rename to stage0/stdlib/Std/Data/BinomialHeap/Basic.c index cb7e3c985b..f2e854fc34 100644 --- a/stage0/stdlib/Init/Data/BinomialHeap/Basic.c +++ b/stage0/stdlib/Std/Data/BinomialHeap/Basic.c @@ -1,6 +1,6 @@ // Lean compiler output -// Module: Init.Data.BinomialHeap.Basic -// Imports: Init.Data.List +// Module: Std.Data.BinomialHeap.Basic +// Imports: Init Init.Data.List #include #if defined(__clang__) #pragma clang diagnostic ignored "-Wunused-parameter" @@ -13,75 +13,75 @@ #ifdef __cplusplus extern "C" { #endif -lean_object* l_BinomialHeapImp_head_x3f(lean_object*); -lean_object* l_BinomialHeapImp_findMin___rarg(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_BinomialHeap_insert___rarg(lean_object*, lean_object*, lean_object*); -lean_object* l_BinomialHeap_tail(lean_object*); -lean_object* l_BinomialHeapImp_toList___main(lean_object*); -lean_object* l_BinomialHeap_tail___rarg(lean_object*, lean_object*); -lean_object* l_BinomialHeap_head___rarg___boxed(lean_object*, lean_object*, lean_object*); -lean_object* l_BinomialHeapImp_tail___rarg(lean_object*, lean_object*); -lean_object* l_mkBinomialHeap(lean_object*, lean_object*); -lean_object* l_BinomialHeapImp_head(lean_object*); +lean_object* l_Std_BinomialHeapImp_merge___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l_Std_BinomialHeapImp_hRank___rarg(lean_object*); +lean_object* l_Std_BinomialHeapImp_toList___main(lean_object*); +lean_object* l_Std_BinomialHeapImp_findMin___main(lean_object*); +lean_object* l_Std_BinomialHeap_singleton___boxed(lean_object*, lean_object*); +lean_object* l_Std_BinomialHeap_head___rarg___boxed(lean_object*, lean_object*, lean_object*); +lean_object* l_Std_BinomialHeapImp_findMin(lean_object*); +lean_object* l_Std_BinomialHeapImp_head_x3f(lean_object*); +lean_object* l_List_foldl___main___at_Std_BinomialHeapImp_tail___spec__2(lean_object*); +lean_object* l_Std_BinomialHeapImp_findMin___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Std_BinomialHeapImp_isEmpty___rarg___boxed(lean_object*); lean_object* l_List_append___rarg(lean_object*, lean_object*); -lean_object* l_BinomialHeapImp_mergeNodes___rarg(lean_object*, lean_object*, lean_object*); -lean_object* l_BinomialHeapImp_singleton(lean_object*); -lean_object* l_BinomialHeap_empty___boxed(lean_object*, lean_object*); -lean_object* l_BinomialHeapImp_findMin(lean_object*); -lean_object* l_List_foldl___main___at_BinomialHeapImp_tail___spec__2(lean_object*); -uint8_t l_BinomialHeapImp_isEmpty___rarg(lean_object*); +lean_object* l_Std_BinomialHeap_insert(lean_object*); +lean_object* l_Std_BinomialHeapImp_combine___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l_Std_BinomialHeap_head_x3f(lean_object*); +lean_object* l_Std_BinomialHeapImp_mergeNodes(lean_object*); +lean_object* l_Std_BinomialHeap_head___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l_Std_BinomialHeapImp_findMin___rarg(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Std_BinomialHeap_insert___rarg(lean_object*, lean_object*, lean_object*); +uint8_t l_Std_BinomialHeapImp_isEmpty___rarg(lean_object*); +lean_object* l_Std_BinomialHeapImp_singleton(lean_object*); +lean_object* l_Std_BinomialHeapImp_mergeNodes___rarg(lean_object*, lean_object*, lean_object*); lean_object* lean_nat_add(lean_object*, lean_object*); -lean_object* l_List_foldl___main___at_BinomialHeapImp_tail___spec__1(lean_object*); -lean_object* l_List_foldl___main___at_BinomialHeapImp_tail___spec__1___rarg(lean_object*, lean_object*, lean_object*); -lean_object* l_BinomialHeapImp_mergeNodes___main(lean_object*); -lean_object* l_BinomialHeap_isEmpty(lean_object*, lean_object*); -lean_object* l_BinomialHeapImp_isEmpty___rarg___boxed(lean_object*); +uint8_t l_Std_BinomialHeap_isEmpty___rarg(lean_object*); +lean_object* l_Std_BinomialHeap_head_x3f___rarg(lean_object*, lean_object*); +lean_object* l_Std_BinomialHeap_toList(lean_object*); +lean_object* l_Std_BinomialHeapImp_head(lean_object*); +lean_object* l_Std_BinomialHeapImp_toList___rarg(lean_object*, lean_object*); +lean_object* l_Std_BinomialHeap_isEmpty(lean_object*, lean_object*); +lean_object* l_Std_BinomialHeap_empty___boxed(lean_object*, lean_object*); uint8_t lean_nat_dec_eq(lean_object*, lean_object*); -lean_object* l_BinomialHeap_isEmpty___rarg___boxed(lean_object*); -lean_object* l_BinomialHeap_toList(lean_object*); -lean_object* l_BinomialHeapImp_hRank___rarg(lean_object*); +lean_object* l_Std_BinomialHeapImp_head___rarg___lambda__1(lean_object*, lean_object*, lean_object*); +lean_object* l_Std_BinomialHeap_merge___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l_Std_BinomialHeap_head(lean_object*); +lean_object* l_Std_BinomialHeapImp_toList(lean_object*); +lean_object* l_Std_BinomialHeapImp_toList___main___rarg(lean_object*, lean_object*); +lean_object* l_List_foldl___main___at_Std_BinomialHeapImp_tail___spec__1(lean_object*); +lean_object* l_List_foldl___main___at_Std_BinomialHeapImp_tail___spec__2___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_List_foldl___main___rarg(lean_object*, lean_object*, lean_object*); -lean_object* l_BinomialHeapImp_mergeNodes___main___rarg(lean_object*, lean_object*, lean_object*); -lean_object* l_BinomialHeap_merge(lean_object*); -lean_object* l_BinomialHeap_empty(lean_object*, lean_object*); -lean_object* l_BinomialHeapImp_combine(lean_object*); -lean_object* l_BinomialHeapImp_toList___main___rarg(lean_object*, lean_object*); -lean_object* l_BinomialHeapImp_merge___rarg(lean_object*, lean_object*, lean_object*); -lean_object* l_BinomialHeapImp_head___rarg(lean_object*, lean_object*, lean_object*); -lean_object* l_BinomialHeapImp_merge(lean_object*); -lean_object* l_BinomialHeap_isEmpty___boxed(lean_object*, lean_object*); -lean_object* l_BinomialHeapImp_combine___rarg(lean_object*, lean_object*, lean_object*); -lean_object* l_List_foldl___main___at_BinomialHeapImp_tail___spec__2___rarg(lean_object*, lean_object*, lean_object*); -lean_object* l_BinomialHeap_head(lean_object*); +lean_object* l_Std_BinomialHeap_singleton(lean_object*, lean_object*); +lean_object* l_Std_BinomialHeapImp_isEmpty(lean_object*); +lean_object* l_Std_mkBinomialHeap___boxed(lean_object*, lean_object*); +lean_object* l_Std_BinomialHeapImp_head___rarg___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_List_eraseIdx___main___rarg(lean_object*, lean_object*); -lean_object* l_BinomialHeap_singleton___boxed(lean_object*, lean_object*); -lean_object* l_BinomialHeapImp_Inhabited(lean_object*); -lean_object* l_BinomialHeap_merge___rarg(lean_object*, lean_object*, lean_object*); -lean_object* l_BinomialHeap_singleton(lean_object*, lean_object*); -lean_object* l_BinomialHeap_head_x3f___rarg(lean_object*, lean_object*); -lean_object* l_BinomialHeapImp_tail(lean_object*); -lean_object* l_BinomialHeap_head_x3f(lean_object*); -uint8_t l_BinomialHeap_isEmpty___rarg(lean_object*); -lean_object* l_BinomialHeapImp_findMin___main(lean_object*); -lean_object* l_BinomialHeapImp_hRank(lean_object*); -lean_object* l_BinomialHeapImp_head_x3f___rarg(lean_object*, lean_object*); -lean_object* l_BinomialHeap_toList___rarg(lean_object*, lean_object*); -lean_object* l_BinomialHeapImp_mergeNodes(lean_object*); -lean_object* l_BinomialHeap_insert(lean_object*); -lean_object* l_BinomialHeap_head___rarg(lean_object*, lean_object*, lean_object*); -lean_object* l_BinomialHeapImp_findMin___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_BinomialHeapImp_singleton___rarg(lean_object*); -lean_object* l_BinomialHeapImp_toList___rarg(lean_object*, lean_object*); -lean_object* l_BinomialHeapImp_hRank___rarg___boxed(lean_object*); -lean_object* l_BinomialHeapImp_head___rarg___boxed(lean_object*, lean_object*, lean_object*); -lean_object* l_BinomialHeapImp_isEmpty(lean_object*); -lean_object* l_mkBinomialHeap___boxed(lean_object*, lean_object*); -lean_object* l_BinomialHeapImp_head___rarg___lambda__1(lean_object*, lean_object*, lean_object*); -lean_object* l_BinomialHeap_singleton___rarg(lean_object*); -lean_object* l_BinomialHeapImp_head_x3f___rarg___lambda__1(lean_object*, lean_object*, lean_object*); -lean_object* l_BinomialHeapImp_toList(lean_object*); +lean_object* l_Std_BinomialHeapImp_mergeNodes___main(lean_object*); +lean_object* l_Std_BinomialHeapImp_head_x3f___rarg___lambda__1(lean_object*, lean_object*, lean_object*); +lean_object* l_Std_BinomialHeap_toList___rarg(lean_object*, lean_object*); +lean_object* l_Std_BinomialHeapImp_hRank(lean_object*); +lean_object* l_Std_BinomialHeapImp_merge(lean_object*); +lean_object* l_Std_BinomialHeapImp_head___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l_Std_BinomialHeapImp_Inhabited(lean_object*); +lean_object* l_Std_BinomialHeapImp_tail(lean_object*); +lean_object* l_Std_BinomialHeap_tail___rarg(lean_object*, lean_object*); +lean_object* l_Std_BinomialHeapImp_hRank___rarg___boxed(lean_object*); +lean_object* l_Std_BinomialHeapImp_head_x3f___rarg(lean_object*, lean_object*); +lean_object* l_Std_mkBinomialHeap(lean_object*, lean_object*); +lean_object* l_Std_BinomialHeap_isEmpty___boxed(lean_object*, lean_object*); +lean_object* l_Std_BinomialHeap_isEmpty___rarg___boxed(lean_object*); +lean_object* l_Std_BinomialHeap_merge(lean_object*); +lean_object* l_Std_BinomialHeap_empty(lean_object*, lean_object*); +lean_object* l_Std_BinomialHeapImp_combine(lean_object*); +lean_object* l_List_foldl___main___at_Std_BinomialHeapImp_tail___spec__1___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l_Std_BinomialHeapImp_tail___rarg(lean_object*, lean_object*); +lean_object* l_Std_BinomialHeapImp_mergeNodes___main___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l_Std_BinomialHeapImp_singleton___rarg(lean_object*); +lean_object* l_Std_BinomialHeap_singleton___rarg(lean_object*); +lean_object* l_Std_BinomialHeap_tail(lean_object*); uint8_t lean_nat_dec_lt(lean_object*, lean_object*); -lean_object* l_BinomialHeapImp_Inhabited(lean_object* x_1) { +lean_object* l_Std_BinomialHeapImp_Inhabited(lean_object* x_1) { _start: { lean_object* x_2; @@ -89,7 +89,7 @@ x_2 = lean_box(0); return x_2; } } -lean_object* l_BinomialHeapImp_hRank___rarg(lean_object* x_1) { +lean_object* l_Std_BinomialHeapImp_hRank___rarg(lean_object* x_1) { _start: { if (lean_obj_tag(x_1) == 0) @@ -108,24 +108,24 @@ return x_4; } } } -lean_object* l_BinomialHeapImp_hRank(lean_object* x_1) { +lean_object* l_Std_BinomialHeapImp_hRank(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_BinomialHeapImp_hRank___rarg___boxed), 1, 0); +x_2 = lean_alloc_closure((void*)(l_Std_BinomialHeapImp_hRank___rarg___boxed), 1, 0); return x_2; } } -lean_object* l_BinomialHeapImp_hRank___rarg___boxed(lean_object* x_1) { +lean_object* l_Std_BinomialHeapImp_hRank___rarg___boxed(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = l_BinomialHeapImp_hRank___rarg(x_1); +x_2 = l_Std_BinomialHeapImp_hRank___rarg(x_1); lean_dec(x_1); return x_2; } } -uint8_t l_BinomialHeapImp_isEmpty___rarg(lean_object* x_1) { +uint8_t l_Std_BinomialHeapImp_isEmpty___rarg(lean_object* x_1) { _start: { if (lean_obj_tag(x_1) == 0) @@ -142,25 +142,25 @@ return x_3; } } } -lean_object* l_BinomialHeapImp_isEmpty(lean_object* x_1) { +lean_object* l_Std_BinomialHeapImp_isEmpty(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_BinomialHeapImp_isEmpty___rarg___boxed), 1, 0); +x_2 = lean_alloc_closure((void*)(l_Std_BinomialHeapImp_isEmpty___rarg___boxed), 1, 0); return x_2; } } -lean_object* l_BinomialHeapImp_isEmpty___rarg___boxed(lean_object* x_1) { +lean_object* l_Std_BinomialHeapImp_isEmpty___rarg___boxed(lean_object* x_1) { _start: { uint8_t x_2; lean_object* x_3; -x_2 = l_BinomialHeapImp_isEmpty___rarg(x_1); +x_2 = l_Std_BinomialHeapImp_isEmpty___rarg(x_1); lean_dec(x_1); x_3 = lean_box(x_2); return x_3; } } -lean_object* l_BinomialHeapImp_singleton___rarg(lean_object* x_1) { +lean_object* l_Std_BinomialHeapImp_singleton___rarg(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; @@ -178,15 +178,15 @@ lean_ctor_set(x_6, 0, x_5); return x_6; } } -lean_object* l_BinomialHeapImp_singleton(lean_object* x_1) { +lean_object* l_Std_BinomialHeapImp_singleton(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_BinomialHeapImp_singleton___rarg), 1, 0); +x_2 = lean_alloc_closure((void*)(l_Std_BinomialHeapImp_singleton___rarg), 1, 0); return x_2; } } -lean_object* l_BinomialHeapImp_combine___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Std_BinomialHeapImp_combine___rarg(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_10; uint8_t x_11; @@ -323,15 +323,15 @@ return x_49; } } } -lean_object* l_BinomialHeapImp_combine(lean_object* x_1) { +lean_object* l_Std_BinomialHeapImp_combine(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_BinomialHeapImp_combine___rarg), 3, 0); +x_2 = lean_alloc_closure((void*)(l_Std_BinomialHeapImp_combine___rarg), 3, 0); return x_2; } } -lean_object* l_BinomialHeapImp_mergeNodes___main___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Std_BinomialHeapImp_mergeNodes___main___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { if (lean_obj_tag(x_2) == 0) @@ -381,23 +381,23 @@ if (x_14 == 0) lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18; lean_dec(x_2); lean_inc(x_1); -x_15 = l_BinomialHeapImp_combine___rarg(x_1, x_4, x_6); +x_15 = l_Std_BinomialHeapImp_combine___rarg(x_1, x_4, x_6); x_16 = lean_ctor_get(x_15, 1); lean_inc(x_16); -x_17 = l_BinomialHeapImp_hRank___rarg(x_5); +x_17 = l_Std_BinomialHeapImp_hRank___rarg(x_5); x_18 = lean_nat_dec_eq(x_16, x_17); lean_dec(x_17); if (x_18 == 0) { lean_object* x_19; uint8_t x_20; -x_19 = l_BinomialHeapImp_hRank___rarg(x_7); +x_19 = l_Std_BinomialHeapImp_hRank___rarg(x_7); x_20 = lean_nat_dec_eq(x_16, x_19); lean_dec(x_19); lean_dec(x_16); if (x_20 == 0) { lean_object* x_21; -x_21 = l_BinomialHeapImp_mergeNodes___main___rarg(x_1, x_5, x_7); +x_21 = l_Std_BinomialHeapImp_mergeNodes___main___rarg(x_1, x_5, x_7); lean_ctor_set(x_3, 1, x_21); lean_ctor_set(x_3, 0, x_15); return x_3; @@ -414,7 +414,7 @@ goto _start; else { lean_object* x_23; uint8_t x_24; -x_23 = l_BinomialHeapImp_hRank___rarg(x_7); +x_23 = l_Std_BinomialHeapImp_hRank___rarg(x_7); x_24 = lean_nat_dec_eq(x_16, x_23); lean_dec(x_23); lean_dec(x_16); @@ -427,7 +427,7 @@ goto _start; else { lean_object* x_26; -x_26 = l_BinomialHeapImp_mergeNodes___main___rarg(x_1, x_5, x_7); +x_26 = l_Std_BinomialHeapImp_mergeNodes___main___rarg(x_1, x_5, x_7); lean_ctor_set(x_3, 1, x_26); lean_ctor_set(x_3, 0, x_15); return x_3; @@ -439,7 +439,7 @@ else lean_object* x_27; lean_dec(x_5); lean_dec(x_4); -x_27 = l_BinomialHeapImp_mergeNodes___main___rarg(x_1, x_7, x_2); +x_27 = l_Std_BinomialHeapImp_mergeNodes___main___rarg(x_1, x_7, x_2); lean_ctor_set(x_3, 1, x_27); return x_3; } @@ -456,23 +456,23 @@ if (x_28 == 0) lean_object* x_29; lean_object* x_30; lean_object* x_31; uint8_t x_32; lean_dec(x_2); lean_inc(x_1); -x_29 = l_BinomialHeapImp_combine___rarg(x_1, x_4, x_6); +x_29 = l_Std_BinomialHeapImp_combine___rarg(x_1, x_4, x_6); x_30 = lean_ctor_get(x_29, 1); lean_inc(x_30); -x_31 = l_BinomialHeapImp_hRank___rarg(x_5); +x_31 = l_Std_BinomialHeapImp_hRank___rarg(x_5); x_32 = lean_nat_dec_eq(x_30, x_31); lean_dec(x_31); if (x_32 == 0) { lean_object* x_33; uint8_t x_34; -x_33 = l_BinomialHeapImp_hRank___rarg(x_7); +x_33 = l_Std_BinomialHeapImp_hRank___rarg(x_7); x_34 = lean_nat_dec_eq(x_30, x_33); lean_dec(x_33); lean_dec(x_30); if (x_34 == 0) { lean_object* x_35; lean_object* x_36; -x_35 = l_BinomialHeapImp_mergeNodes___main___rarg(x_1, x_5, x_7); +x_35 = l_Std_BinomialHeapImp_mergeNodes___main___rarg(x_1, x_5, x_7); x_36 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_36, 0, x_29); lean_ctor_set(x_36, 1, x_35); @@ -492,7 +492,7 @@ goto _start; else { lean_object* x_39; uint8_t x_40; -x_39 = l_BinomialHeapImp_hRank___rarg(x_7); +x_39 = l_Std_BinomialHeapImp_hRank___rarg(x_7); x_40 = lean_nat_dec_eq(x_30, x_39); lean_dec(x_39); lean_dec(x_30); @@ -509,7 +509,7 @@ goto _start; else { lean_object* x_43; lean_object* x_44; -x_43 = l_BinomialHeapImp_mergeNodes___main___rarg(x_1, x_5, x_7); +x_43 = l_Std_BinomialHeapImp_mergeNodes___main___rarg(x_1, x_5, x_7); x_44 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_44, 0, x_29); lean_ctor_set(x_44, 1, x_43); @@ -522,7 +522,7 @@ else lean_object* x_45; lean_object* x_46; lean_dec(x_5); lean_dec(x_4); -x_45 = l_BinomialHeapImp_mergeNodes___main___rarg(x_1, x_7, x_2); +x_45 = l_Std_BinomialHeapImp_mergeNodes___main___rarg(x_1, x_7, x_2); x_46 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_46, 0, x_6); lean_ctor_set(x_46, 1, x_45); @@ -539,7 +539,7 @@ lean_dec(x_7); lean_dec(x_6); lean_dec(x_2); lean_inc(x_3); -x_47 = l_BinomialHeapImp_mergeNodes___main___rarg(x_1, x_5, x_3); +x_47 = l_Std_BinomialHeapImp_mergeNodes___main___rarg(x_1, x_5, x_3); x_48 = !lean_is_exclusive(x_3); if (x_48 == 0) { @@ -566,31 +566,31 @@ return x_51; } } } -lean_object* l_BinomialHeapImp_mergeNodes___main(lean_object* x_1) { +lean_object* l_Std_BinomialHeapImp_mergeNodes___main(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_BinomialHeapImp_mergeNodes___main___rarg), 3, 0); +x_2 = lean_alloc_closure((void*)(l_Std_BinomialHeapImp_mergeNodes___main___rarg), 3, 0); return x_2; } } -lean_object* l_BinomialHeapImp_mergeNodes___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Std_BinomialHeapImp_mergeNodes___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { lean_object* x_4; -x_4 = l_BinomialHeapImp_mergeNodes___main___rarg(x_1, x_2, x_3); +x_4 = l_Std_BinomialHeapImp_mergeNodes___main___rarg(x_1, x_2, x_3); return x_4; } } -lean_object* l_BinomialHeapImp_mergeNodes(lean_object* x_1) { +lean_object* l_Std_BinomialHeapImp_mergeNodes(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_BinomialHeapImp_mergeNodes___rarg), 3, 0); +x_2 = lean_alloc_closure((void*)(l_Std_BinomialHeapImp_mergeNodes___rarg), 3, 0); return x_2; } } -lean_object* l_BinomialHeapImp_merge___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Std_BinomialHeapImp_merge___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { if (lean_obj_tag(x_2) == 0) @@ -616,7 +616,7 @@ if (x_5 == 0) { lean_object* x_6; lean_object* x_7; x_6 = lean_ctor_get(x_3, 0); -x_7 = l_BinomialHeapImp_mergeNodes___main___rarg(x_1, x_4, x_6); +x_7 = l_Std_BinomialHeapImp_mergeNodes___main___rarg(x_1, x_4, x_6); lean_ctor_set(x_3, 0, x_7); return x_3; } @@ -626,7 +626,7 @@ lean_object* x_8; lean_object* x_9; lean_object* x_10; x_8 = lean_ctor_get(x_3, 0); lean_inc(x_8); lean_dec(x_3); -x_9 = l_BinomialHeapImp_mergeNodes___main___rarg(x_1, x_4, x_8); +x_9 = l_Std_BinomialHeapImp_mergeNodes___main___rarg(x_1, x_4, x_8); x_10 = lean_alloc_ctor(1, 1, 0); lean_ctor_set(x_10, 0, x_9); return x_10; @@ -635,15 +635,15 @@ return x_10; } } } -lean_object* l_BinomialHeapImp_merge(lean_object* x_1) { +lean_object* l_Std_BinomialHeapImp_merge(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_BinomialHeapImp_merge___rarg), 3, 0); +x_2 = lean_alloc_closure((void*)(l_Std_BinomialHeapImp_merge___rarg), 3, 0); return x_2; } } -lean_object* l_BinomialHeapImp_head_x3f___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Std_BinomialHeapImp_head_x3f___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { if (lean_obj_tag(x_2) == 0) @@ -719,7 +719,7 @@ return x_16; } } } -lean_object* l_BinomialHeapImp_head_x3f___rarg(lean_object* x_1, lean_object* x_2) { +lean_object* l_Std_BinomialHeapImp_head_x3f___rarg(lean_object* x_1, lean_object* x_2) { _start: { if (lean_obj_tag(x_2) == 0) @@ -735,7 +735,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; x_4 = lean_ctor_get(x_2, 0); lean_inc(x_4); lean_dec(x_2); -x_5 = lean_alloc_closure((void*)(l_BinomialHeapImp_head_x3f___rarg___lambda__1), 3, 1); +x_5 = lean_alloc_closure((void*)(l_Std_BinomialHeapImp_head_x3f___rarg___lambda__1), 3, 1); lean_closure_set(x_5, 0, x_1); x_6 = lean_box(0); x_7 = l_List_foldl___main___rarg(x_5, x_6, x_4); @@ -743,15 +743,15 @@ return x_7; } } } -lean_object* l_BinomialHeapImp_head_x3f(lean_object* x_1) { +lean_object* l_Std_BinomialHeapImp_head_x3f(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_BinomialHeapImp_head_x3f___rarg), 2, 0); +x_2 = lean_alloc_closure((void*)(l_Std_BinomialHeapImp_head_x3f___rarg), 2, 0); return x_2; } } -lean_object* l_BinomialHeapImp_head___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Std_BinomialHeapImp_head___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { lean_object* x_4; lean_object* x_5; uint8_t x_6; @@ -775,7 +775,7 @@ return x_2; } } } -lean_object* l_BinomialHeapImp_head___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Std_BinomialHeapImp_head___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { if (lean_obj_tag(x_3) == 0) @@ -804,7 +804,7 @@ lean_inc(x_5); x_6 = lean_ctor_get(x_4, 1); lean_inc(x_6); lean_dec(x_4); -x_7 = lean_alloc_closure((void*)(l_BinomialHeapImp_head___rarg___lambda__1), 3, 1); +x_7 = lean_alloc_closure((void*)(l_Std_BinomialHeapImp_head___rarg___lambda__1), 3, 1); lean_closure_set(x_7, 0, x_2); x_8 = lean_ctor_get(x_5, 0); lean_inc(x_8); @@ -815,24 +815,24 @@ return x_9; } } } -lean_object* l_BinomialHeapImp_head(lean_object* x_1) { +lean_object* l_Std_BinomialHeapImp_head(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_BinomialHeapImp_head___rarg___boxed), 3, 0); +x_2 = lean_alloc_closure((void*)(l_Std_BinomialHeapImp_head___rarg___boxed), 3, 0); return x_2; } } -lean_object* l_BinomialHeapImp_head___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Std_BinomialHeapImp_head___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { lean_object* x_4; -x_4 = l_BinomialHeapImp_head___rarg(x_1, x_2, x_3); +x_4 = l_Std_BinomialHeapImp_head___rarg(x_1, x_2, x_3); lean_dec(x_1); return x_4; } } -lean_object* l_BinomialHeapImp_findMin___main___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +lean_object* l_Std_BinomialHeapImp_findMin___main___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { if (lean_obj_tag(x_2) == 0) @@ -908,31 +908,31 @@ goto _start; } } } -lean_object* l_BinomialHeapImp_findMin___main(lean_object* x_1) { +lean_object* l_Std_BinomialHeapImp_findMin___main(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_BinomialHeapImp_findMin___main___rarg), 4, 0); +x_2 = lean_alloc_closure((void*)(l_Std_BinomialHeapImp_findMin___main___rarg), 4, 0); return x_2; } } -lean_object* l_BinomialHeapImp_findMin___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +lean_object* l_Std_BinomialHeapImp_findMin___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { lean_object* x_5; -x_5 = l_BinomialHeapImp_findMin___main___rarg(x_1, x_2, x_3, x_4); +x_5 = l_Std_BinomialHeapImp_findMin___main___rarg(x_1, x_2, x_3, x_4); return x_5; } } -lean_object* l_BinomialHeapImp_findMin(lean_object* x_1) { +lean_object* l_Std_BinomialHeapImp_findMin(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_BinomialHeapImp_findMin___rarg), 4, 0); +x_2 = lean_alloc_closure((void*)(l_Std_BinomialHeapImp_findMin___rarg), 4, 0); return x_2; } } -lean_object* l_List_foldl___main___at_BinomialHeapImp_tail___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_List_foldl___main___at_Std_BinomialHeapImp_tail___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { if (lean_obj_tag(x_3) == 0) @@ -949,22 +949,22 @@ x_5 = lean_ctor_get(x_3, 1); lean_inc(x_5); lean_dec(x_3); lean_inc(x_1); -x_6 = l_BinomialHeapImp_merge___rarg(x_1, x_2, x_4); +x_6 = l_Std_BinomialHeapImp_merge___rarg(x_1, x_2, x_4); x_2 = x_6; x_3 = x_5; goto _start; } } } -lean_object* l_List_foldl___main___at_BinomialHeapImp_tail___spec__1(lean_object* x_1) { +lean_object* l_List_foldl___main___at_Std_BinomialHeapImp_tail___spec__1(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_List_foldl___main___at_BinomialHeapImp_tail___spec__1___rarg), 3, 0); +x_2 = lean_alloc_closure((void*)(l_List_foldl___main___at_Std_BinomialHeapImp_tail___spec__1___rarg), 3, 0); return x_2; } } -lean_object* l_List_foldl___main___at_BinomialHeapImp_tail___spec__2___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_List_foldl___main___at_Std_BinomialHeapImp_tail___spec__2___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { if (lean_obj_tag(x_3) == 0) @@ -981,22 +981,22 @@ x_5 = lean_ctor_get(x_3, 1); lean_inc(x_5); lean_dec(x_3); lean_inc(x_1); -x_6 = l_BinomialHeapImp_merge___rarg(x_1, x_2, x_4); +x_6 = l_Std_BinomialHeapImp_merge___rarg(x_1, x_2, x_4); x_2 = x_6; x_3 = x_5; goto _start; } } } -lean_object* l_List_foldl___main___at_BinomialHeapImp_tail___spec__2(lean_object* x_1) { +lean_object* l_List_foldl___main___at_Std_BinomialHeapImp_tail___spec__2(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_List_foldl___main___at_BinomialHeapImp_tail___spec__2___rarg), 3, 0); +x_2 = lean_alloc_closure((void*)(l_List_foldl___main___at_Std_BinomialHeapImp_tail___spec__2___rarg), 3, 0); return x_2; } } -lean_object* l_BinomialHeapImp_tail___rarg(lean_object* x_1, lean_object* x_2) { +lean_object* l_Std_BinomialHeapImp_tail___rarg(lean_object* x_1, lean_object* x_2) { _start: { if (lean_obj_tag(x_2) == 0) @@ -1050,7 +1050,7 @@ lean_inc(x_10); x_11 = lean_ctor_get(x_8, 1); lean_inc(x_11); lean_dec(x_8); -x_12 = l_List_foldl___main___at_BinomialHeapImp_tail___spec__1___rarg(x_1, x_10, x_11); +x_12 = l_List_foldl___main___at_Std_BinomialHeapImp_tail___spec__1___rarg(x_1, x_10, x_11); return x_12; } } @@ -1065,7 +1065,7 @@ lean_ctor_set(x_15, 0, x_13); lean_ctor_set(x_15, 1, x_14); x_16 = lean_unsigned_to_nat(1u); lean_inc(x_1); -x_17 = l_BinomialHeapImp_findMin___main___rarg(x_1, x_6, x_16, x_15); +x_17 = l_Std_BinomialHeapImp_findMin___main___rarg(x_1, x_6, x_16, x_15); x_18 = lean_ctor_get(x_17, 0); lean_inc(x_18); x_19 = lean_ctor_get(x_17, 1); @@ -1077,7 +1077,7 @@ lean_ctor_set(x_2, 0, x_20); x_21 = lean_ctor_get(x_18, 2); lean_inc(x_21); lean_dec(x_18); -x_22 = l_List_foldl___main___at_BinomialHeapImp_tail___spec__2___rarg(x_1, x_2, x_21); +x_22 = l_List_foldl___main___at_Std_BinomialHeapImp_tail___spec__2___rarg(x_1, x_2, x_21); return x_22; } } @@ -1124,7 +1124,7 @@ lean_inc(x_29); x_30 = lean_ctor_get(x_27, 1); lean_inc(x_30); lean_dec(x_27); -x_31 = l_List_foldl___main___at_BinomialHeapImp_tail___spec__1___rarg(x_1, x_29, x_30); +x_31 = l_List_foldl___main___at_Std_BinomialHeapImp_tail___spec__1___rarg(x_1, x_29, x_30); return x_31; } } @@ -1139,7 +1139,7 @@ lean_ctor_set(x_34, 0, x_32); lean_ctor_set(x_34, 1, x_33); x_35 = lean_unsigned_to_nat(1u); lean_inc(x_1); -x_36 = l_BinomialHeapImp_findMin___main___rarg(x_1, x_25, x_35, x_34); +x_36 = l_Std_BinomialHeapImp_findMin___main___rarg(x_1, x_25, x_35, x_34); x_37 = lean_ctor_get(x_36, 0); lean_inc(x_37); x_38 = lean_ctor_get(x_36, 1); @@ -1152,7 +1152,7 @@ lean_ctor_set(x_40, 0, x_39); x_41 = lean_ctor_get(x_37, 2); lean_inc(x_41); lean_dec(x_37); -x_42 = l_List_foldl___main___at_BinomialHeapImp_tail___spec__2___rarg(x_1, x_40, x_41); +x_42 = l_List_foldl___main___at_Std_BinomialHeapImp_tail___spec__2___rarg(x_1, x_40, x_41); return x_42; } } @@ -1160,15 +1160,15 @@ return x_42; } } } -lean_object* l_BinomialHeapImp_tail(lean_object* x_1) { +lean_object* l_Std_BinomialHeapImp_tail(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_BinomialHeapImp_tail___rarg), 2, 0); +x_2 = lean_alloc_closure((void*)(l_Std_BinomialHeapImp_tail___rarg), 2, 0); return x_2; } } -lean_object* l_BinomialHeapImp_toList___main___rarg(lean_object* x_1, lean_object* x_2) { +lean_object* l_Std_BinomialHeapImp_toList___main___rarg(lean_object* x_1, lean_object* x_2) { _start: { if (lean_obj_tag(x_2) == 0) @@ -1183,7 +1183,7 @@ else lean_object* x_4; lean_inc(x_2); lean_inc(x_1); -x_4 = l_BinomialHeapImp_head_x3f___rarg(x_1, x_2); +x_4 = l_Std_BinomialHeapImp_head_x3f___rarg(x_1, x_2); if (lean_obj_tag(x_4) == 0) { lean_object* x_5; @@ -1199,8 +1199,8 @@ x_6 = lean_ctor_get(x_4, 0); lean_inc(x_6); lean_dec(x_4); lean_inc(x_1); -x_7 = l_BinomialHeapImp_tail___rarg(x_1, x_2); -x_8 = l_BinomialHeapImp_toList___main___rarg(x_1, x_7); +x_7 = l_Std_BinomialHeapImp_tail___rarg(x_1, x_2); +x_8 = l_Std_BinomialHeapImp_toList___main___rarg(x_1, x_7); x_9 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_9, 0, x_6); lean_ctor_set(x_9, 1, x_8); @@ -1209,31 +1209,31 @@ return x_9; } } } -lean_object* l_BinomialHeapImp_toList___main(lean_object* x_1) { +lean_object* l_Std_BinomialHeapImp_toList___main(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_BinomialHeapImp_toList___main___rarg), 2, 0); +x_2 = lean_alloc_closure((void*)(l_Std_BinomialHeapImp_toList___main___rarg), 2, 0); return x_2; } } -lean_object* l_BinomialHeapImp_toList___rarg(lean_object* x_1, lean_object* x_2) { +lean_object* l_Std_BinomialHeapImp_toList___rarg(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; -x_3 = l_BinomialHeapImp_toList___main___rarg(x_1, x_2); +x_3 = l_Std_BinomialHeapImp_toList___main___rarg(x_1, x_2); return x_3; } } -lean_object* l_BinomialHeapImp_toList(lean_object* x_1) { +lean_object* l_Std_BinomialHeapImp_toList(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_BinomialHeapImp_toList___rarg), 2, 0); +x_2 = lean_alloc_closure((void*)(l_Std_BinomialHeapImp_toList___rarg), 2, 0); return x_2; } } -lean_object* l_mkBinomialHeap(lean_object* x_1, lean_object* x_2) { +lean_object* l_Std_mkBinomialHeap(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; @@ -1241,16 +1241,16 @@ x_3 = lean_box(0); return x_3; } } -lean_object* l_mkBinomialHeap___boxed(lean_object* x_1, lean_object* x_2) { +lean_object* l_Std_mkBinomialHeap___boxed(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; -x_3 = l_mkBinomialHeap(x_1, x_2); +x_3 = l_Std_mkBinomialHeap(x_1, x_2); lean_dec(x_2); return x_3; } } -lean_object* l_BinomialHeap_empty(lean_object* x_1, lean_object* x_2) { +lean_object* l_Std_BinomialHeap_empty(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; @@ -1258,187 +1258,191 @@ x_3 = lean_box(0); return x_3; } } -lean_object* l_BinomialHeap_empty___boxed(lean_object* x_1, lean_object* x_2) { +lean_object* l_Std_BinomialHeap_empty___boxed(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; -x_3 = l_BinomialHeap_empty(x_1, x_2); +x_3 = l_Std_BinomialHeap_empty(x_1, x_2); lean_dec(x_2); return x_3; } } -uint8_t l_BinomialHeap_isEmpty___rarg(lean_object* x_1) { +uint8_t l_Std_BinomialHeap_isEmpty___rarg(lean_object* x_1) { _start: { uint8_t x_2; -x_2 = l_BinomialHeapImp_isEmpty___rarg(x_1); +x_2 = l_Std_BinomialHeapImp_isEmpty___rarg(x_1); return x_2; } } -lean_object* l_BinomialHeap_isEmpty(lean_object* x_1, lean_object* x_2) { +lean_object* l_Std_BinomialHeap_isEmpty(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; -x_3 = lean_alloc_closure((void*)(l_BinomialHeap_isEmpty___rarg___boxed), 1, 0); +x_3 = lean_alloc_closure((void*)(l_Std_BinomialHeap_isEmpty___rarg___boxed), 1, 0); return x_3; } } -lean_object* l_BinomialHeap_isEmpty___rarg___boxed(lean_object* x_1) { +lean_object* l_Std_BinomialHeap_isEmpty___rarg___boxed(lean_object* x_1) { _start: { uint8_t x_2; lean_object* x_3; -x_2 = l_BinomialHeap_isEmpty___rarg(x_1); +x_2 = l_Std_BinomialHeap_isEmpty___rarg(x_1); lean_dec(x_1); x_3 = lean_box(x_2); return x_3; } } -lean_object* l_BinomialHeap_isEmpty___boxed(lean_object* x_1, lean_object* x_2) { +lean_object* l_Std_BinomialHeap_isEmpty___boxed(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; -x_3 = l_BinomialHeap_isEmpty(x_1, x_2); +x_3 = l_Std_BinomialHeap_isEmpty(x_1, x_2); lean_dec(x_2); return x_3; } } -lean_object* l_BinomialHeap_singleton___rarg(lean_object* x_1) { +lean_object* l_Std_BinomialHeap_singleton___rarg(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = l_BinomialHeapImp_singleton___rarg(x_1); +x_2 = l_Std_BinomialHeapImp_singleton___rarg(x_1); return x_2; } } -lean_object* l_BinomialHeap_singleton(lean_object* x_1, lean_object* x_2) { +lean_object* l_Std_BinomialHeap_singleton(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; -x_3 = lean_alloc_closure((void*)(l_BinomialHeap_singleton___rarg), 1, 0); +x_3 = lean_alloc_closure((void*)(l_Std_BinomialHeap_singleton___rarg), 1, 0); return x_3; } } -lean_object* l_BinomialHeap_singleton___boxed(lean_object* x_1, lean_object* x_2) { +lean_object* l_Std_BinomialHeap_singleton___boxed(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; -x_3 = l_BinomialHeap_singleton(x_1, x_2); +x_3 = l_Std_BinomialHeap_singleton(x_1, x_2); lean_dec(x_2); return x_3; } } -lean_object* l_BinomialHeap_merge___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Std_BinomialHeap_merge___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { lean_object* x_4; -x_4 = l_BinomialHeapImp_merge___rarg(x_1, x_2, x_3); +x_4 = l_Std_BinomialHeapImp_merge___rarg(x_1, x_2, x_3); return x_4; } } -lean_object* l_BinomialHeap_merge(lean_object* x_1) { +lean_object* l_Std_BinomialHeap_merge(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_BinomialHeap_merge___rarg), 3, 0); +x_2 = lean_alloc_closure((void*)(l_Std_BinomialHeap_merge___rarg), 3, 0); return x_2; } } -lean_object* l_BinomialHeap_head___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Std_BinomialHeap_head___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { lean_object* x_4; -x_4 = l_BinomialHeapImp_head___rarg(x_2, x_1, x_3); +x_4 = l_Std_BinomialHeapImp_head___rarg(x_2, x_1, x_3); return x_4; } } -lean_object* l_BinomialHeap_head(lean_object* x_1) { +lean_object* l_Std_BinomialHeap_head(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_BinomialHeap_head___rarg___boxed), 3, 0); +x_2 = lean_alloc_closure((void*)(l_Std_BinomialHeap_head___rarg___boxed), 3, 0); return x_2; } } -lean_object* l_BinomialHeap_head___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Std_BinomialHeap_head___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { lean_object* x_4; -x_4 = l_BinomialHeap_head___rarg(x_1, x_2, x_3); +x_4 = l_Std_BinomialHeap_head___rarg(x_1, x_2, x_3); lean_dec(x_2); return x_4; } } -lean_object* l_BinomialHeap_head_x3f___rarg(lean_object* x_1, lean_object* x_2) { +lean_object* l_Std_BinomialHeap_head_x3f___rarg(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; -x_3 = l_BinomialHeapImp_head_x3f___rarg(x_1, x_2); +x_3 = l_Std_BinomialHeapImp_head_x3f___rarg(x_1, x_2); return x_3; } } -lean_object* l_BinomialHeap_head_x3f(lean_object* x_1) { +lean_object* l_Std_BinomialHeap_head_x3f(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_BinomialHeap_head_x3f___rarg), 2, 0); +x_2 = lean_alloc_closure((void*)(l_Std_BinomialHeap_head_x3f___rarg), 2, 0); return x_2; } } -lean_object* l_BinomialHeap_tail___rarg(lean_object* x_1, lean_object* x_2) { +lean_object* l_Std_BinomialHeap_tail___rarg(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; -x_3 = l_BinomialHeapImp_tail___rarg(x_1, x_2); +x_3 = l_Std_BinomialHeapImp_tail___rarg(x_1, x_2); return x_3; } } -lean_object* l_BinomialHeap_tail(lean_object* x_1) { +lean_object* l_Std_BinomialHeap_tail(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_BinomialHeap_tail___rarg), 2, 0); +x_2 = lean_alloc_closure((void*)(l_Std_BinomialHeap_tail___rarg), 2, 0); return x_2; } } -lean_object* l_BinomialHeap_insert___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Std_BinomialHeap_insert___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { lean_object* x_4; lean_object* x_5; -x_4 = l_BinomialHeapImp_singleton___rarg(x_2); -x_5 = l_BinomialHeapImp_merge___rarg(x_1, x_4, x_3); +x_4 = l_Std_BinomialHeapImp_singleton___rarg(x_2); +x_5 = l_Std_BinomialHeapImp_merge___rarg(x_1, x_4, x_3); return x_5; } } -lean_object* l_BinomialHeap_insert(lean_object* x_1) { +lean_object* l_Std_BinomialHeap_insert(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_BinomialHeap_insert___rarg), 3, 0); +x_2 = lean_alloc_closure((void*)(l_Std_BinomialHeap_insert___rarg), 3, 0); return x_2; } } -lean_object* l_BinomialHeap_toList___rarg(lean_object* x_1, lean_object* x_2) { +lean_object* l_Std_BinomialHeap_toList___rarg(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; -x_3 = l_BinomialHeapImp_toList___main___rarg(x_1, x_2); +x_3 = l_Std_BinomialHeapImp_toList___main___rarg(x_1, x_2); return x_3; } } -lean_object* l_BinomialHeap_toList(lean_object* x_1) { +lean_object* l_Std_BinomialHeap_toList(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_BinomialHeap_toList___rarg), 2, 0); +x_2 = lean_alloc_closure((void*)(l_Std_BinomialHeap_toList___rarg), 2, 0); return x_2; } } +lean_object* initialize_Init(lean_object*); lean_object* initialize_Init_Data_List(lean_object*); static bool _G_initialized = false; -lean_object* initialize_Init_Data_BinomialHeap_Basic(lean_object* w) { +lean_object* initialize_Std_Data_BinomialHeap_Basic(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); res = initialize_Init_Data_List(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res);