Skip to content

Commit d741ef3

Browse files
committed
chore: delete unused C++ file
1 parent 455fd0b commit d741ef3

File tree

22 files changed

+0
-204
lines changed

22 files changed

+0
-204
lines changed

src/Lean/ProjFns.lean

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -36,13 +36,11 @@ def ProjectionFunctionInfo.fromClassEx (info : ProjectionFunctionInfo) : Bool :=
3636

3737
builtin_initialize projectionFnInfoExt : MapDeclarationExtension ProjectionFunctionInfo ← mkMapDeclarationExtension
3838

39-
@[export lean_add_projection_info]
4039
def addProjectionFnInfo (env : Environment) (projName : Name) (ctorName : Name) (numParams : Nat) (i : Nat) (fromClass : Bool) : Environment :=
4140
projectionFnInfoExt.insert env projName { ctorName, numParams, i, fromClass }
4241

4342
namespace Environment
4443

45-
@[export lean_get_projection_info]
4644
def getProjectionFnInfo? (env : Environment) (projName : Name) : Option ProjectionFunctionInfo :=
4745
projectionFnInfoExt.find? env projName
4846

src/library/CMakeLists.txt

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@ add_library(library OBJECT expr_lt.cpp
33
module.cpp dynlib.cpp replace_visitor.cpp num.cpp
44
class.cpp util.cpp print.cpp annotation.cpp
55
reducible.cpp init_module.cpp
6-
projection.cpp
76
aux_recursors.cpp
87
profiling.cpp time_task.cpp
98
formatter.cpp

src/library/projection.cpp

Lines changed: 0 additions & 35 deletions
This file was deleted.

src/library/projection.h

Lines changed: 0 additions & 56 deletions
This file was deleted.

src/library/util.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,6 @@ Author: Leonardo de Moura
1717
#include "library/suffixes.h"
1818
#include "library/annotation.h"
1919
#include "library/constants.h"
20-
#include "library/projection.h"
2120
#include "library/replace_visitor.h"
2221
#include "library/num.h"
2322
#include "githash.h" // NOLINT

tests/pkg/ver_clash/DiamondExample-A/.gitignore

Lines changed: 0 additions & 1 deletion
This file was deleted.

tests/pkg/ver_clash/DiamondExample-A/DiamondExampleA.lean

Lines changed: 0 additions & 2 deletions
This file was deleted.

tests/pkg/ver_clash/DiamondExample-A/DiamondExampleA/Ring/Defs.lean

Lines changed: 0 additions & 9 deletions
This file was deleted.

tests/pkg/ver_clash/DiamondExample-A/DiamondExampleA/Ring/Lemmas.lean

Lines changed: 0 additions & 13 deletions
This file was deleted.

tests/pkg/ver_clash/DiamondExample-A/lakefile.toml

Lines changed: 0 additions & 6 deletions
This file was deleted.

0 commit comments

Comments
 (0)