mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-20 20:04:23 +00:00
Compare commits
3 Commits
fix-window
...
expr_eq_ca
| Author | SHA1 | Date | |
|---|---|---|---|
|
|
34fe8d3805 | ||
|
|
ea84c036a7 | ||
|
|
6b57dceb04 |
@@ -94,10 +94,7 @@ def emitCInitName (n : Name) : M Unit :=
|
||||
def shouldExport (n : Name) : Bool :=
|
||||
-- HACK: exclude symbols very unlikely to be used by the interpreter or other consumers of
|
||||
-- libleanshared to avoid Windows symbol limit
|
||||
!(`Lean.Compiler.LCNF).isPrefixOf n &&
|
||||
!(`Lean.IR).isPrefixOf n &&
|
||||
-- Lean.Server.findModuleRefs is used in Verso
|
||||
(!(`Lean.Server).isPrefixOf n || n == `Lean.Server.findModuleRefs)
|
||||
!(`Lean.Compiler.LCNF).isPrefixOf n && !(`Lean.IR).isPrefixOf n && !(`Lean.Server).isPrefixOf n
|
||||
|
||||
def emitFnDeclAux (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M Unit := do
|
||||
let ps := decl.params
|
||||
|
||||
BIN
stage0/src/kernel/environment.cpp
generated
BIN
stage0/src/kernel/environment.cpp
generated
Binary file not shown.
BIN
stage0/src/kernel/expr_eq_fn.cpp
generated
BIN
stage0/src/kernel/expr_eq_fn.cpp
generated
Binary file not shown.
BIN
stage0/src/kernel/replace_fn.cpp
generated
BIN
stage0/src/kernel/replace_fn.cpp
generated
Binary file not shown.
BIN
stage0/src/runtime/sharecommon.cpp
generated
BIN
stage0/src/runtime/sharecommon.cpp
generated
Binary file not shown.
BIN
stage0/src/runtime/sharecommon.h
generated
BIN
stage0/src/runtime/sharecommon.h
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Data.c
generated
BIN
stage0/stdlib/Init/Data.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Data/Array/Lemmas.c
generated
BIN
stage0/stdlib/Init/Data/Array/Lemmas.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Data/Array/TakeDrop.c
generated
BIN
stage0/stdlib/Init/Data/Array/TakeDrop.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Data/BitVec/Bitblast.c
generated
BIN
stage0/stdlib/Init/Data/BitVec/Bitblast.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Data/List.c
generated
BIN
stage0/stdlib/Init/Data/List.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Data/List/Attach.c
generated
BIN
stage0/stdlib/Init/Data/List/Attach.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Data/List/Count.c
generated
BIN
stage0/stdlib/Init/Data/List/Count.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Data/List/Erase.c
generated
BIN
stage0/stdlib/Init/Data/List/Erase.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Data/List/Find.c
generated
BIN
stage0/stdlib/Init/Data/List/Find.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Data/List/Lemmas.c
generated
BIN
stage0/stdlib/Init/Data/List/Lemmas.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Data/List/MinMax.c
generated
BIN
stage0/stdlib/Init/Data/List/MinMax.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Data/List/Monadic.c
generated
BIN
stage0/stdlib/Init/Data/List/Monadic.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Data/List/Nat.c
generated
BIN
stage0/stdlib/Init/Data/List/Nat.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Data/List/Nat/Basic.c
generated
BIN
stage0/stdlib/Init/Data/List/Nat/Basic.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Data/List/Nat/Pairwise.c
generated
BIN
stage0/stdlib/Init/Data/List/Nat/Pairwise.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Data/List/Nat/Range.c
generated
BIN
stage0/stdlib/Init/Data/List/Nat/Range.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Data/List/Nat/TakeDrop.c
generated
BIN
stage0/stdlib/Init/Data/List/Nat/TakeDrop.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Data/List/Pairwise.c
generated
BIN
stage0/stdlib/Init/Data/List/Pairwise.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Data/List/Sublist.c
generated
BIN
stage0/stdlib/Init/Data/List/Sublist.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Data/List/TakeDrop.c
generated
BIN
stage0/stdlib/Init/Data/List/TakeDrop.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Data/List/Zip.c
generated
BIN
stage0/stdlib/Init/Data/List/Zip.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Data/Subtype.c
generated
BIN
stage0/stdlib/Init/Data/Subtype.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Meta.c
generated
BIN
stage0/stdlib/Init/Meta.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/MetaTypes.c
generated
BIN
stage0/stdlib/Init/MetaTypes.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Omega/Constraint.c
generated
BIN
stage0/stdlib/Init/Omega/Constraint.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/Omega/IntList.c
generated
BIN
stage0/stdlib/Init/Omega/IntList.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/ShareCommon.c
generated
BIN
stage0/stdlib/Init/ShareCommon.c
generated
Binary file not shown.
BIN
stage0/stdlib/Init/System/IO.c
generated
BIN
stage0/stdlib/Init/System/IO.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lake/Build/Module.c
generated
BIN
stage0/stdlib/Lake/Build/Module.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lake/Build/Trace.c
generated
BIN
stage0/stdlib/Lake/Build/Trace.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lake/Load/Lean/Elab.c
generated
BIN
stage0/stdlib/Lake/Load/Lean/Elab.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Class.c
generated
BIN
stage0/stdlib/Lean/Class.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Compiler/CSimpAttr.c
generated
BIN
stage0/stdlib/Lean/Compiler/CSimpAttr.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Compiler/IR/EmitC.c
generated
BIN
stage0/stdlib/Lean/Compiler/IR/EmitC.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Compiler/LCNF/AlphaEqv.c
generated
BIN
stage0/stdlib/Lean/Compiler/LCNF/AlphaEqv.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Compiler/LCNF/AuxDeclCache.c
generated
BIN
stage0/stdlib/Lean/Compiler/LCNF/AuxDeclCache.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Compiler/LCNF/Basic.c
generated
BIN
stage0/stdlib/Lean/Compiler/LCNF/Basic.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Compiler/LCNF/Check.c
generated
BIN
stage0/stdlib/Lean/Compiler/LCNF/Check.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Compiler/LCNF/CompilerM.c
generated
BIN
stage0/stdlib/Lean/Compiler/LCNF/CompilerM.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Compiler/LCNF/DeclHash.c
generated
BIN
stage0/stdlib/Lean/Compiler/LCNF/DeclHash.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Compiler/LCNF/ElimDead.c
generated
BIN
stage0/stdlib/Lean/Compiler/LCNF/ElimDead.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Compiler/LCNF/ElimDeadBranches.c
generated
BIN
stage0/stdlib/Lean/Compiler/LCNF/ElimDeadBranches.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Compiler/LCNF/FVarUtil.c
generated
BIN
stage0/stdlib/Lean/Compiler/LCNF/FVarUtil.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Compiler/LCNF/FixedParams.c
generated
BIN
stage0/stdlib/Lean/Compiler/LCNF/FixedParams.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Compiler/LCNF/FloatLetIn.c
generated
BIN
stage0/stdlib/Lean/Compiler/LCNF/FloatLetIn.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Compiler/LCNF/JoinPoints.c
generated
BIN
stage0/stdlib/Lean/Compiler/LCNF/JoinPoints.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Compiler/LCNF/LCtx.c
generated
BIN
stage0/stdlib/Lean/Compiler/LCNF/LCtx.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Compiler/LCNF/Level.c
generated
BIN
stage0/stdlib/Lean/Compiler/LCNF/Level.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Compiler/LCNF/Simp/FunDeclInfo.c
generated
BIN
stage0/stdlib/Lean/Compiler/LCNF/Simp/FunDeclInfo.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Compiler/LCNF/Simp/Main.c
generated
BIN
stage0/stdlib/Lean/Compiler/LCNF/Simp/Main.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Compiler/LCNF/Specialize.c
generated
BIN
stage0/stdlib/Lean/Compiler/LCNF/Specialize.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Compiler/LCNF/Testing.c
generated
BIN
stage0/stdlib/Lean/Compiler/LCNF/Testing.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Compiler/LCNF/ToLCNF.c
generated
BIN
stage0/stdlib/Lean/Compiler/LCNF/ToLCNF.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/CoreM.c
generated
BIN
stage0/stdlib/Lean/CoreM.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Data/JsonRpc.c
generated
BIN
stage0/stdlib/Lean/Data/JsonRpc.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Data/KVMap.c
generated
BIN
stage0/stdlib/Lean/Data/KVMap.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Data/Lsp/Basic.c
generated
BIN
stage0/stdlib/Lean/Data/Lsp/Basic.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Data/Lsp/Capabilities.c
generated
BIN
stage0/stdlib/Lean/Data/Lsp/Capabilities.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Data/Lsp/CodeActions.c
generated
BIN
stage0/stdlib/Lean/Data/Lsp/CodeActions.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Data/Lsp/Diagnostics.c
generated
BIN
stage0/stdlib/Lean/Data/Lsp/Diagnostics.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Data/Lsp/Extra.c
generated
BIN
stage0/stdlib/Lean/Data/Lsp/Extra.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Data/Lsp/InitShutdown.c
generated
BIN
stage0/stdlib/Lean/Data/Lsp/InitShutdown.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Data/Lsp/Internal.c
generated
BIN
stage0/stdlib/Lean/Data/Lsp/Internal.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Data/Lsp/Ipc.c
generated
BIN
stage0/stdlib/Lean/Data/Lsp/Ipc.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Data/Lsp/LanguageFeatures.c
generated
BIN
stage0/stdlib/Lean/Data/Lsp/LanguageFeatures.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Data/Lsp/TextSync.c
generated
BIN
stage0/stdlib/Lean/Data/Lsp/TextSync.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Data/Lsp/Workspace.c
generated
BIN
stage0/stdlib/Lean/Data/Lsp/Workspace.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Data/Rat.c
generated
BIN
stage0/stdlib/Lean/Data/Rat.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Declaration.c
generated
BIN
stage0/stdlib/Lean/Declaration.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Elab/App.c
generated
BIN
stage0/stdlib/Lean/Elab/App.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Elab/Binders.c
generated
BIN
stage0/stdlib/Lean/Elab/Binders.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Elab/Calc.c
generated
BIN
stage0/stdlib/Lean/Elab/Calc.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Elab/DeclUtil.c
generated
BIN
stage0/stdlib/Lean/Elab/DeclUtil.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Elab/Deriving/DecEq.c
generated
BIN
stage0/stdlib/Lean/Elab/Deriving/DecEq.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Elab/Import.c
generated
BIN
stage0/stdlib/Lean/Elab/Import.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Elab/Inductive.c
generated
BIN
stage0/stdlib/Lean/Elab/Inductive.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Elab/InfoTree/Main.c
generated
BIN
stage0/stdlib/Lean/Elab/InfoTree/Main.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Elab/MutualDef.c
generated
BIN
stage0/stdlib/Lean/Elab/MutualDef.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Elab/PreDefinition/Basic.c
generated
BIN
stage0/stdlib/Lean/Elab/PreDefinition/Basic.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Elab/PreDefinition/Main.c
generated
BIN
stage0/stdlib/Lean/Elab/PreDefinition/Main.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Elab/PreDefinition/Structural/Main.c
generated
BIN
stage0/stdlib/Lean/Elab/PreDefinition/Structural/Main.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Elab/PreDefinition/WF/Main.c
generated
BIN
stage0/stdlib/Lean/Elab/PreDefinition/WF/Main.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Elab/StructInst.c
generated
BIN
stage0/stdlib/Lean/Elab/StructInst.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Elab/Structure.c
generated
BIN
stage0/stdlib/Lean/Elab/Structure.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Elab/Syntax.c
generated
BIN
stage0/stdlib/Lean/Elab/Syntax.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Elab/SyntheticMVars.c
generated
BIN
stage0/stdlib/Lean/Elab/SyntheticMVars.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Elab/Tactic/Cache.c
generated
BIN
stage0/stdlib/Lean/Elab/Tactic/Cache.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Elab/Tactic/Ext.c
generated
BIN
stage0/stdlib/Lean/Elab/Tactic/Ext.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Elab/Tactic/Omega/Core.c
generated
BIN
stage0/stdlib/Lean/Elab/Tactic/Omega/Core.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Elab/Tactic/Omega/MinNatAbs.c
generated
BIN
stage0/stdlib/Lean/Elab/Tactic/Omega/MinNatAbs.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Elab/Tactic/RCases.c
generated
BIN
stage0/stdlib/Lean/Elab/Tactic/RCases.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Elab/Tactic/Simpa.c
generated
BIN
stage0/stdlib/Lean/Elab/Tactic/Simpa.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Elab/Term.c
generated
BIN
stage0/stdlib/Lean/Elab/Term.c
generated
Binary file not shown.
BIN
stage0/stdlib/Lean/Environment.c
generated
BIN
stage0/stdlib/Lean/Environment.c
generated
Binary file not shown.
Some files were not shown because too many files have changed in this diff Show More
Reference in New Issue
Block a user