Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 0 additions & 2 deletions src/Lean/ProjFns.lean
Original file line number Diff line number Diff line change
Expand Up @@ -36,13 +36,11 @@ def ProjectionFunctionInfo.fromClassEx (info : ProjectionFunctionInfo) : Bool :=

builtin_initialize projectionFnInfoExt : MapDeclarationExtension ProjectionFunctionInfo ← mkMapDeclarationExtension

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

namespace Environment

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

Expand Down
1 change: 0 additions & 1 deletion src/library/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@ add_library(library OBJECT expr_lt.cpp
module.cpp dynlib.cpp replace_visitor.cpp num.cpp
class.cpp util.cpp print.cpp annotation.cpp
reducible.cpp init_module.cpp
projection.cpp
aux_recursors.cpp
profiling.cpp time_task.cpp
formatter.cpp
Expand Down
35 changes: 0 additions & 35 deletions src/library/projection.cpp

This file was deleted.

56 changes: 0 additions & 56 deletions src/library/projection.h

This file was deleted.

1 change: 0 additions & 1 deletion src/library/util.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,6 @@ Author: Leonardo de Moura
#include "library/suffixes.h"
#include "library/annotation.h"
#include "library/constants.h"
#include "library/projection.h"
#include "library/replace_visitor.h"
#include "library/num.h"
#include "githash.h" // NOLINT
Expand Down
Loading