hub / github.com/JetBrains/arend-lib
github.com/JetBrains/arend-lib @v1.10.0
Chat with this repo
1,046 symbols
3,040 edges
136 files
5 documented · 0%
What it actually does AI analysis from the code graph — generated when you open this
loading…
README
Arend Standard Library
Arend is a theorem prover based on Homotopy Type Theory. Visit arend-lang.github.io for more information about the Arend language.
Extension points exported contracts — how you extend this code
EquationSolver (Interface)(no doc) [5 implementers]
meta/src/main/java/org/arend/lib/meta/equation/EquationSolver.java
FunctionMatcher (Interface)
(no doc) [4 implementers]
meta/src/main/java/org/arend/lib/meta/equation/binop_matcher/FunctionMatcher.java
DataFactory (Interface)
(no doc) [4 implementers]
meta/src/main/java/org/arend/lib/meta/equation/datafactory/DataFactory.java
BinaryRelationClosure (Interface)
(no doc) [4 implementers]
meta/src/main/java/org/arend/lib/meta/closure/BinaryRelationClosure.java
SimplificationRule (Interface)
(no doc) [3 implementers]
meta/src/main/java/org/arend/lib/meta/simplify/SimplificationRule.java
Core symbols most depended-on inside this repo
getcalled by 869
meta/src/main/java/org/arend/lib/util/Lazy.java
add
called by 610
meta/src/main/java/org/arend/lib/util/algorithms/polynomials/Ring.java
getRef
called by 397
meta/src/main/java/org/arend/lib/util/Utils.java
getExpression
called by 258
meta/src/main/java/org/arend/lib/meta/cong/CongVisitor.java
isEmpty
called by 173
meta/src/main/java/org/arend/lib/meta/ContradictionMeta.java
getBinding
called by 133
meta/src/main/java/org/arend/lib/pattern/ArendPattern.java
getParameters
called by 57
meta/src/main/java/org/arend/lib/pattern/ArendPattern.java
getTypeExpr
called by 45
meta/src/main/java/org/arend/lib/pattern/PatternUtils.java
Shape
Languages
Java100%
Modules by API surface
meta/src/main/java/org/arend/lib/meta/closure/CongruenceClosure.java40 symbols
meta/src/main/java/org/arend/lib/meta/equation/MonoidSolver.java35 symbols
meta/src/main/java/org/arend/lib/meta/SimpCoeMeta.java34 symbols
meta/src/main/java/org/arend/lib/meta/ExtMeta.java33 symbols
meta/src/main/java/org/arend/lib/util/Utils.java32 symbols
meta/src/main/java/org/arend/lib/meta/linear/LinearSolver.java29 symbols
meta/src/main/java/org/arend/lib/meta/ContradictionMeta.java26 symbols
meta/src/main/java/org/arend/lib/meta/cong/CongVisitor.java25 symbols
meta/src/main/java/org/arend/lib/meta/equation/RingSolver.java24 symbols
meta/src/main/java/org/arend/lib/meta/linear/TermCompiler.java23 symbols
meta/src/main/java/org/arend/lib/meta/MatchingCasesMeta.java22 symbols
meta/src/main/java/org/arend/lib/pattern/PatternUtils.java19 symbols
For agents
$ claude mcp add arend-lib \
-- python -m otcore.mcp_server <graph>