Commit 03a6e58

Lean stage0 autoupdater

committed

chore: update stage0

1 parent 72ddc47 commit 03a6e58Copy full SHA for 03a6e58

354 files changed

+59972

-66123

lines changed

stage0
- src/library
  - module.cpp
- stdlib
  - Init
    - Data/String
      - Basic.c
    - Grind
      - Ordered
        Linarith.c
      - Ring
        CommSolver.c
    - System
      - IO.c
      - Uri.c
  - Lake
    - Build
    - CLI
      - Init.c
      - Main.c
      - Translate
        Lean.c
        Toml.c
    - Config
    - DSL
      - Meta.c
    - Load
      - Lean
        Elab.c
      - Manifest.c
      - Toml.c
      - Workspace.c
    - Toml/Elab
      - Value.c
    - Util
  - Lean
    - AddDecl.c
    - Attributes.c
    - Class.c
    - Compiler
      - CSimpAttr.c
      - IR
        Borrow.c
        ElimDeadBranches.c
        EmitC.c
        EmitLLVM.c
        EmitUtil.c
        ExpandResetReuse.c
        RC.c
        ToIR.c
        Toposort.c
      - LCNF
        CSE.c
        ElimDeadBranches.c
        ExtractClosed.c
        FixedParams.c
        Internalize.c
        JoinPoints.c
        LCtx.c
        LambdaLifting.c
        Level.c
        Main.c
        PrettyPrinter.c
        Probing.c
        ReduceArity.c
        Simp.c
        Simp
        ConstantFold.c
        FunDeclInfo.c
        InlineCandidate.c
        JpCases.c
        Main.c
        SimpM.c
        Specialize.c
        StructProjCases.c
        ToDecl.c
        ToLCNF.c
        ToMono.c
    - CoreM.c
    - Data
      - JsonRpc.c
      - Json
        Basic.c
        Parser.c
      - Lsp
        Basic.c
        InitShutdown.c
        Ipc.c
      - NameMap
        Basic.c
      - SMap.c
      - SSet.c
      - Xml
        Parser.c
    - DocString
      - Add.c
      - Links.c
    - Elab
      - App.c
      - Binders.c
      - BuiltinCommand.c
      - BuiltinEvalCommand.c
      - BuiltinNotation.c
      - BuiltinTerm.c
      - Calc.c
      - Command.c
      - DeclNameGen.c
      - Declaration.c
      - Deriving
        FromToJson.c
      - DocString.c
      - DocString
        Builtin.c
        Builtin
        Keywords.c
      - Do
        Basic.c
      - ErrorExplanation.c
      - GuardMsgs.c
      - Inductive.c
      - InfoTree
        Main.c
      - MacroArgUtil.c
      - Match.c
      - MutualDef.c
      - MutualInductive.c
      - PatternVar.c
      - PreDefinition
        Basic.c
        Eqns.c
        FixedParams.c
        Main.c
        PartialFixpoint
        Induction.c
        Structural
        BRecOn.c
        Eqns.c
        FindRecArg.c
        IndPred.c
        Main.c
        Preprocess.c
        SmartUnfolding.c
        TerminationHint.c
        TerminationMeasure.c
        WF
        Fix.c
        FloatRecApp.c
        GuessLex.c
        PackMutual.c
        Preprocess.c
        Unfold.c
      - Quotation.c
      - StructInst.c
      - Structure.c
      - Syntax.c
      - SyntheticMVars.c
      - Tactic
        BVDecide
        Frontend
        Attr.c
        BVDecide.c
        BVDecide
        Reflect.c
        Normalize.c
        Normalize
        AC.c
        AndFlatten.c
        Basic.c
        EmbeddedConstraint.c
        Enums.c
        IntToBitVec.c
        TypeAnalysis.c
        LRAT
        Trim.c
        Basic.c
        Conv
        Pattern.c
        Doc.c
        Do
        LetElim.c
        ProofMode
        MGoal.c
        VCGen.c
        VCGen
        Basic.c
        Split.c
        SuggestInvariant.c
        ElabTerm.c
        Ext.c
        FalseOrByContra.c
        Grind
        BuiltinTactic.c
        ShowState.c
        Induction.c
        NormCast.c
        Omega
        Core.c
        Frontend.c
        OmegaM.c
        RCases.c
        Rewrite.c
        SimpTrace.c
        Simpa.c
        Try.c
      - Term
        TermElabM.c
    - Environment.c
    - ErrorExplanation.c
    - ExtraModUses.c
    - IdentifierSuggestion.c
    - KeyedDeclsAttribute.c
    - LabelAttribute.c
    - Language
      - Lean.c
    - LibrarySuggestions
      - Basic.c
      - SymbolFrequency.c
    - Linter
      - ConstructorAsVariable.c
      - MissingDocs.c
      - UnusedSimpArgs.c
      - UnusedVariables.c
    - MetavarContext.c
    - Meta
      - AbstractMVars.c
      - AbstractNestedProofs.c
      - Basic.c
      - BinderNameHint.c
      - Canonicalizer.c
      - Check.c
      - Closure.c
      - Coe.c
      - CollectMVars.c
      - Constructions
        CasesOnSameCtor.c
      - Eval.c
      - ExprDefEq.c
      - ForEachExpr.c
      - FunInfo.c
      - GeneralizeVars.c
      - Hint.c
      - IndPredBelow.c
      - InferType.c
      - Injective.c
      - LazyDiscrTree.c
      - LetToHave.c
      - Match
        CaseArraySizes.c
        CaseValues.c
        Match.c
        MatchEqs.c
        MatcherApp
        Basic.c
        MatcherInfo.c
        NamedPatterns.c
        SimpH.c
        SolveOverlap.c
      - PProdN.c
      - Reduce.c
      - Structure.c
      - SynthInstance.c
      - Tactic
        AC
        Main.c
        Acyclic.c
        Assert.c
        Cases.c
        Cleanup.c
        Clear.c
        Delta.c
        ElimInfo.c
        ExposeNames.c
        FunInd.c
        FunIndCollect.c
        Grind
        AC
        Eq.c
        Proof.c
        Util.c
        Anchor.c
        Arith.c
        Arith
        CommRing
        EqCnstr.c
        Proof.c
        Cutsat
        EqCnstr.c
        Model.c
        Proof.c
        Search.c
        Util.c
        Linear
        Model.c
        OfNatModule.c
        Proof.c
        Search.c
        ModelUtil.c
        Propagate.c
        Simproc.c
        Util.c
        Canon.c
        CasesMatch.c
        EMatch.c
        EMatchAction.c
        EMatchTheorem.c
        EMatchTheoremParam.c
        EqResolution.c
        Internalize.c
        MBTC.c
        Main.c
        MarkNestedSubsingletons.c
        MatchDiscrOnly.c
        PropagatorAttr.c
        ProveEq.c
        Simp.c
        Split.c
        SynthInstance.c
        Types.c
        Util.c
        VarRename.c
        Induction.c
        Intro.c
        Lets.c
        NormCast.c
        Replace.c
        Revert.c
        Rewrites.c
        Rfl.c
        Simp
        Arith/Int
        Basic.c
        Simp.c
        LoopProtection.c
        Main.c
        Rewrite.c
        SimpCongrTheorems.c
        SimpTheorems.c
        Simproc.c
        Types.c
        Split.c
        SplitIf.c
        Subst.c
        Try
        Collect.c
      - Transform.c
      - WHNF.c
    - Parser
      - Types.c
    - PrettyPrinter.c
    - PrettyPrinter/Delaborator
      - Builtins.c
      - TopDownAnalyze.c
    - ReducibilityAttrs.c
    - ResolveName.c
    - ScopedEnvExtension.c
    - Server
      - CodeActions
        UnknownIdentifier.c
      - Completion.c
      - Completion
        CompletionCollectors.c
        CompletionInfoSelection.c
        EligibleHeaderDecls.c
      - FileWorker.c
      - FileWorker
        SemanticHighlighting.c
      - GoTo.c
      - References.c
      - Test
        Runner.c
      - Watchdog.c
    - Shell.c
    - Structure.c
    - Util
      - CollectFVars.c
      - CollectLevelMVars.c
      - CollectLevelParams.c
      - CollectLooseBVars.c
      - CollectMVars.c
      - Diff.c
      - FVarSubset.c
      - FoldConsts.c
      - ForEachExpr.c
      - ForEachExprWhere.c
      - LeanOptions.c
      - MonadCache.c
      - OccursCheck.c
      - Profiler.c
      - SCC.c
      - SortExprs.c
      - Trace.c
    - Widget
      - InteractiveGoal.c
  - Std
    - Data
      - DHashMap
        Basic.c
        Internal
        Defs.c
        RawLemmas.c
        WF.c
        Raw.c
      - DTreeMap/Internal
        Lemmas.c
      - ExtDHashMap
        Basic.c
      - ExtDTreeMap
        Basic.c
      - ExtHashMap
        Basic.c
      - ExtHashSet
        Basic.c
      - ExtTreeMap
        Basic.c
      - ExtTreeSet
        Basic.c
      - HashMap
        Basic.c
        Raw.c
      - HashSet
        Basic.c
        Raw.c
    - Internal/Async
      - System.c
    - Sat/AIG
    - Tactic/BVDecide
      - Bitblast/BVExpr/Circuit/Impl
        Const.c
        Expr.c
        Operations
        ShiftLeft.c
        ShiftRight.c
        ZeroExtend.c
        Substructure.c
      - Reflect.c
    - Time/Format
      - Basic.c

354 files changed

+59972

-66123

lines changed

`‎stage0/src/library/module.cpp‎`

Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

Comments

(0)