Commit bebe1c5

committed

chore: update stage0

1 parent c991bf8 commit bebe1c5Copy full SHA for bebe1c5

361 files changed

+360826

-357786

lines changed

stage0/stdlib
- Init
  - Control/Lawful
    - Instances.c
  - Core.c
  - Data
    - Array
      - Attach.c
      - Lex
        Basic.c
    - ByteArray
      - Basic.c
      - Extra.c
    - List
      - Attach.c
      - Nat
        Modify.c
    - Nat
      - Basic.c
    - Range/Polymorphic
    - Slice
      - Array
        Basic.c
        Iterator.c
      - Notation.c
    - String
      - Basic.c
      - Decode.c
      - Pattern
        Basic.c
        String.c
      - Slice.c
    - ToString
      - Name.c
    - Vector
      - Attach.c
      - Basic.c
  - Meta
    - Defs.c
  - System
    - IO.c
    - Uri.c
- Lake
  - Build
    - Common.c
    - Data.c
    - Executable.c
    - ExternLib.c
    - InputFile.c
    - Library.c
    - Module.c
    - Package.c
    - Run.c
    - Target
      - Fetch.c
    - Trace.c
  - CLI
    - Init.c
    - Translate
      - Lean.c
  - Config
    - Meta.c
  - DSL
    - Meta.c
  - Load
    - Toml.c
  - Util
    - String.c
- Lean
  - AddDecl.c
  - Attributes.c
  - Compiler
    - CSimpAttr.c
    - IR
    - LCNF
  - CoreM.c
  - Data
    - Array.c
    - Json
      - Basic.c
      - Printer.c
    - Lsp
      - Internal.c
    - Options.c
    - Trie.c
  - DocString
    - Add.c
    - Extension.c
    - Links.c
  - Elab
    - App.c
    - Binders.c
    - BindersUtil.c
    - BuiltinCommand.c
    - BuiltinEvalCommand.c
    - BuiltinNotation.c
    - BuiltinTerm.c
    - Command.c
    - ComputedFields.c
    - DeclModifiers.c
    - DeclNameGen.c
    - DeclUtil.c
    - Declaration.c
    - DefView.c
    - Deriving
      - BEq.c
      - Basic.c
      - DecEq.c
      - FromToJson.c
      - Hashable.c
      - Inhabited.c
      - Ord.c
      - Repr.c
      - ToExpr.c
      - Util.c
    - Do.c
    - DocString.c
    - DocString
      - Builtin.c
      - Builtin
        Keywords.c
        Postponed.c
    - ErrorExplanation.c
    - Exception.c
    - Extra.c
    - GuardMsgs.c
    - Import.c
    - Inductive.c
    - InheritDoc.c
    - LetRec.c
    - Macro.c
    - MacroArgUtil.c
    - Match.c
    - Mixfix.c
    - MutualDef.c
    - MutualInductive.c
    - Notation.c
    - PatternVar.c
    - PreDefinition
      - Basic.c
      - EqUnfold.c
      - Eqns.c
      - FixedParams.c
      - Main.c
      - Nonrec
        Eqns.c
      - PartialFixpoint
        Eqns.c
        Induction.c
        Main.c
      - Structural
        BRecOn.c
        Eqns.c
        FindRecArg.c
        IndPred.c
        Main.c
        RecArgInfo.c
        SmartUnfolding.c
      - TerminationHint.c
      - TerminationMeasure.c
      - WF
        Eqns.c
        Fix.c
        GuessLex.c
        Main.c
        PackMutual.c
        Preprocess.c
        Rel.c
        Unfold.c
    - Print.c
    - Quotation.c
    - StructInst.c
    - StructInstHint.c
    - Structure.c
    - Syntax.c
    - SyntheticMVars.c
    - Tactic
      - BVDecide
        Frontend
        BVDecide.c
        Normalize
        AC.c
        Enums.c
        IntToBitVec.c
        Structures.c
        TypeAnalysis.c
        LRAT
        Trim.c
      - Basic.c
      - BuiltinTactic.c
      - Classical.c
      - Config.c
      - Conv
        Basic.c
        Congr.c
      - Do
        LetElim.c
        ProofMode
        Basic.c
        MGoal.c
        Refine.c
        Specialize.c
        Spec.c
        VCGen.c
        VCGen
        Basic.c
        Split.c
      - ElabTerm.c
      - Ext.c
      - Grind
        Basic.c
        Main.c
      - Induction.c
      - Lets.c
      - Monotonicity.c
      - Omega
        Core.c
        Frontend.c
      - RCases.c
      - Rewrite.c
      - Simp.c
      - Split.c
      - Try.c
    - Term
      - TermElabM.c
  - Environment.c
  - ErrorExplanation.c
  - KeyedDeclsAttribute.c
  - Language
    - Basic.c
    - Lean.c
  - Level.c
  - Linter
    - Deprecated.c
    - DocsOnAlt.c
    - MissingDocs.c
    - Sets.c
    - UnusedSimpArgs.c
    - UnusedVariables.c
  - LocalContext.c
  - Message.c
  - MetavarContext.c
  - Meta
    - ACLt.c
    - AbstractNestedProofs.c
    - AppBuilder.c
    - ArgsPacker.c
    - Basic.c
    - Canonicalizer.c
    - Check.c
    - Closure.c
    - CollectMVars.c
    - CongrTheorems.c
    - Constructions
      - BRecOn.c
      - CasesOn.c
      - CasesOnSameCtor.c
      - CtorElim.c
      - NoConfusion.c
      - RecOn.c
    - DiscrTree.c
    - Eqns.c
    - Eval.c
    - ExprDefEq.c
    - ForEachExpr.c
    - FunInfo.c
    - Hint.c
    - IndPredBelow.c
    - InferType.c
    - Injective.c
    - Instances.c
    - LazyDiscrTree.c
    - LetToHave.c
    - Match
      - Match.c
      - MatchEqs.c
      - MatcherApp
        Basic.c
        Transform.c
    - MethodSpecs.c
    - PProdN.c
    - RecursorInfo.c
    - Reduce.c
    - SizeOf.c
    - Structure.c
    - SynthInstance.c
    - Tactic
      - AC
        Main.c
      - Apply.c
      - Assert.c
      - AuxLemma.c
      - Backtrack.c
      - Cases.c
      - Clear.c
      - Constructor.c
      - Contradiction.c
      - ElimInfo.c
      - FunInd.c
      - Grind
        AC
        Eq.c
        Inv.c
        Proof.c
        Arith
        CommRing
        EqCnstr.c
        Inv.c
        Proof.c
        Cutsat
        Proof.c
        Linear
        Inv.c
        Proof.c
        Search.c
        Offset
        Main.c
        Model.c
        Canon.c
        Cases.c
        CasesMatch.c
        Core.c
        EMatch.c
        EMatchTheorem.c
        Ext.c
        Injective.c
        Internalize.c
        Inv.c
        MBTC.c
        MarkNestedSubsingletons.c
        MatchCond.c
        SimpUtil.c
        Types.c
      - Induction.c
      - Injection.c
      - Lets.c
      - LibrarySearch.c
      - NormCast.c
      - Simp
        Attr.c
        Main.c
        Rewrite.c
        SimpAll.c
        SimpTheorems.c
        Simproc.c
        Types.c
      - Split.c
      - SplitIf.c
      - TryThis.c
    - UnificationHint.c
    - WHNF.c
  - MonadEnv.c
  - ParserCompiler.c
  - ParserCompiler
    - Attribute.c
  - PrettyPrinter
    - Basic.c
    - Delaborator
  - Server
    - CodeActions
    - Completion
    - FileWorker
    - InfoUtils.c
    - References.c
    - Rpc
      - RequestHandling.c
  - Structure.c
  - Syntax.c
  - Util
    - Diff.c
    - Profiler.c
  - Widget
    - Diff.c
    - InteractiveDiagnostic.c
    - UserWidget.c
- Std
  - Data
    - ByteSlice.c
    - ExtTreeSet
      - Basic.c
    - Iterators/Producers
      - Range.c
  - Do
    - PredTrans.c
    - Triple
      - SpecLemmas.c
    - WP
      - Basic.c
      - Monad.c
  - Sat/AIG
    - Basic.c
  - Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl
    - Expr.c
  - Time
    - Format
      - Basic.c
    - Zoned/Database
      - Basic.c
      - TzIf.c

361 files changed

+360826

-357786

lines changed

`‎stage0/stdlib/Init/Control/Lawful/Instances.c‎`

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

`‎stage0/stdlib/Init/Core.c‎`

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

Comments

(0)