Path Lines of Code meta/build.gradle.kts 31 meta/settings.gradle.kts 2 meta/src/main/java/org/arend/lib/StdExtension.java 334 meta/src/main/java/org/arend/lib/StdNumberTypechecker.java 64 meta/src/main/java/org/arend/lib/context/Context.java 24 meta/src/main/java/org/arend/lib/context/ContextHelper.java 58 meta/src/main/java/org/arend/lib/context/HidingContext.java 33 meta/src/main/java/org/arend/lib/error/EquationSolverError.java 86 meta/src/main/java/org/arend/lib/error/FieldNotPropError.java 19 meta/src/main/java/org/arend/lib/error/IgnoredArgumentError.java 13 meta/src/main/java/org/arend/lib/error/LinearSolverError.java 45 meta/src/main/java/org/arend/lib/error/MetaDidNotFailError.java 22 meta/src/main/java/org/arend/lib/error/MonoidSolverError.java 64 meta/src/main/java/org/arend/lib/error/SimplifyError.java 32 meta/src/main/java/org/arend/lib/error/SubclassError.java 21 meta/src/main/java/org/arend/lib/error/SubexprError.java 34 meta/src/main/java/org/arend/lib/error/TypeError.java 26 meta/src/main/java/org/arend/lib/goal/ConstructorGoalSolver.java 117 meta/src/main/java/org/arend/lib/goal/StdGoalSolver.java 50 meta/src/main/java/org/arend/lib/key/FieldKey.java 111 meta/src/main/java/org/arend/lib/key/IrreflexivityKey.java 40 meta/src/main/java/org/arend/lib/key/ReflexivityKey.java 31 meta/src/main/java/org/arend/lib/key/TransitivityKey.java 34 meta/src/main/java/org/arend/lib/level/StdLevelProver.java 142 meta/src/main/java/org/arend/lib/meta/ApplyMeta.java 43 meta/src/main/java/org/arend/lib/meta/AssumptionMeta.java 76 meta/src/main/java/org/arend/lib/meta/AtMeta.java 57 meta/src/main/java/org/arend/lib/meta/CasesMeta.java 373 meta/src/main/java/org/arend/lib/meta/ClassExtResolver.java 53 meta/src/main/java/org/arend/lib/meta/ConstructorMeta.java 148 meta/src/main/java/org/arend/lib/meta/ContradictionMeta.java 518 meta/src/main/java/org/arend/lib/meta/DefaultImplMeta.java 78 meta/src/main/java/org/arend/lib/meta/ExistsMeta.java 285 meta/src/main/java/org/arend/lib/meta/ExtMeta.java 735 meta/src/main/java/org/arend/lib/meta/FailsMeta.java 59 meta/src/main/java/org/arend/lib/meta/HidingMeta.java 49 meta/src/main/java/org/arend/lib/meta/InMeta.java 45 meta/src/main/java/org/arend/lib/meta/LaterMeta.java 15 meta/src/main/java/org/arend/lib/meta/MakeConstructorMeta.java 49 meta/src/main/java/org/arend/lib/meta/MatchingCasesMeta.java 1123 meta/src/main/java/org/arend/lib/meta/NormalizationMeta.java 23 meta/src/main/java/org/arend/lib/meta/OrElseMeta.java 37 meta/src/main/java/org/arend/lib/meta/RepeatMeta.java 84 meta/src/main/java/org/arend/lib/meta/RewriteMeta.java 377 meta/src/main/java/org/arend/lib/meta/RunMeta.java 75 meta/src/main/java/org/arend/lib/meta/SIPMeta.java 165 meta/src/main/java/org/arend/lib/meta/SimpCoeMeta.java 477 meta/src/main/java/org/arend/lib/meta/UnfoldLetMeta.java 38 meta/src/main/java/org/arend/lib/meta/UnfoldMeta.java 124 meta/src/main/java/org/arend/lib/meta/UnfoldsMeta.java 50 meta/src/main/java/org/arend/lib/meta/UsingMeta.java 68 meta/src/main/java/org/arend/lib/meta/closure/BinaryRelationClosure.java 7 meta/src/main/java/org/arend/lib/meta/closure/BunchedEquivalenceClosure.java 89 meta/src/main/java/org/arend/lib/meta/closure/CongruenceClosure.java 439 meta/src/main/java/org/arend/lib/meta/closure/EquivalenceClosure.java 66 meta/src/main/java/org/arend/lib/meta/closure/ValuesRelationClosure.java 23 meta/src/main/java/org/arend/lib/meta/cong/CongVisitor.java 379 meta/src/main/java/org/arend/lib/meta/cong/CongruenceMeta.java 126 meta/src/main/java/org/arend/lib/meta/debug/PrintMeta.java 42 meta/src/main/java/org/arend/lib/meta/debug/RandomMeta.java 56 meta/src/main/java/org/arend/lib/meta/debug/TimeMeta.java 27 meta/src/main/java/org/arend/lib/meta/equation/BaseEqualitySolver.java 103 meta/src/main/java/org/arend/lib/meta/equation/EqualitySolver.java 145 meta/src/main/java/org/arend/lib/meta/equation/EquationMeta.java 296 meta/src/main/java/org/arend/lib/meta/equation/EquationSolver.java 57 meta/src/main/java/org/arend/lib/meta/equation/EquivSolver.java 90 meta/src/main/java/org/arend/lib/meta/equation/MonoidSolver.java 771 meta/src/main/java/org/arend/lib/meta/equation/RingSolver.java 310 meta/src/main/java/org/arend/lib/meta/equation/TermCompiler.java 147 meta/src/main/java/org/arend/lib/meta/equation/TransitivitySolver.java 209 meta/src/main/java/org/arend/lib/meta/equation/binop_matcher/DefinitionFunctionMatcher.java 38 meta/src/main/java/org/arend/lib/meta/equation/binop_matcher/ExpressionFunctionMatcher.java 59 meta/src/main/java/org/arend/lib/meta/equation/binop_matcher/FunctionMatcher.java 44 meta/src/main/java/org/arend/lib/meta/equation/binop_matcher/ListFunctionMatcher.java 45 meta/src/main/java/org/arend/lib/meta/equation/binop_matcher/NatFunctionMatcher.java 39 meta/src/main/java/org/arend/lib/meta/equation/datafactory/CategoryDataFactory.java 70 meta/src/main/java/org/arend/lib/meta/equation/datafactory/DataFactory.java 5 meta/src/main/java/org/arend/lib/meta/equation/datafactory/DataFactoryBase.java 61 meta/src/main/java/org/arend/lib/meta/equation/datafactory/GroupDataFactory.java 28 meta/src/main/java/org/arend/lib/meta/equation/datafactory/MonoidDataFactory.java 35 meta/src/main/java/org/arend/lib/meta/equation/datafactory/RingDataFactory.java 29 meta/src/main/java/org/arend/lib/meta/equation/term/CompiledTerm.java 43 meta/src/main/java/org/arend/lib/meta/equation/term/CompositeTerm.java 13 meta/src/main/java/org/arend/lib/meta/equation/term/VarTerm.java 7 meta/src/main/java/org/arend/lib/meta/linear/CompiledTerm.java 10 meta/src/main/java/org/arend/lib/meta/linear/CompiledTerms.java 12 meta/src/main/java/org/arend/lib/meta/linear/Equation.java 19 meta/src/main/java/org/arend/lib/meta/linear/LinearSolver.java 555 meta/src/main/java/org/arend/lib/meta/linear/LinearSolverMeta.java 56 meta/src/main/java/org/arend/lib/meta/linear/TermCompiler.java 306 meta/src/main/java/org/arend/lib/meta/pi_tree/BasePiTree.java 23 meta/src/main/java/org/arend/lib/meta/pi_tree/PathExpression.java 18 meta/src/main/java/org/arend/lib/meta/pi_tree/PiTreeMaker.java 287 meta/src/main/java/org/arend/lib/meta/pi_tree/PiTreeNode.java 11 meta/src/main/java/org/arend/lib/meta/pi_tree/PiTreeRoot.java 21 meta/src/main/java/org/arend/lib/meta/simplify/AbGroupInverseRule.java 120 meta/src/main/java/org/arend/lib/meta/simplify/DoubleNegationRule.java 41 meta/src/main/java/org/arend/lib/meta/simplify/GroupInverseRule.java 154 meta/src/main/java/org/arend/lib/meta/simplify/GroupRuleBase.java 53 meta/src/main/java/org/arend/lib/meta/simplify/IdentityInverseRule.java 41 meta/src/main/java/org/arend/lib/meta/simplify/LocalSimplificationRuleBase.java 127 meta/src/main/java/org/arend/lib/meta/simplify/MonoidIdentityRule.java 58 meta/src/main/java/org/arend/lib/meta/simplify/MulOfNegativesRule.java 52 meta/src/main/java/org/arend/lib/meta/simplify/MultiplicationByZeroRule.java 37 meta/src/main/java/org/arend/lib/meta/simplify/NegationPropagationRule.java 49 meta/src/main/java/org/arend/lib/meta/simplify/SimplificationRule.java 8 meta/src/main/java/org/arend/lib/meta/simplify/Simplifier.java 226 meta/src/main/java/org/arend/lib/meta/simplify/SimplifyMeta.java 64 meta/src/main/java/org/arend/lib/meta/solver/BaseTermCompiler.java 109 meta/src/main/java/org/arend/lib/meta/solver/RingKind.java 2 meta/src/main/java/org/arend/lib/meta/util/MetaInvocationMeta.java 114 meta/src/main/java/org/arend/lib/meta/util/ReplaceSubexpressionsMeta.java 61 meta/src/main/java/org/arend/lib/meta/util/SubstitutionMeta.java 66 meta/src/main/java/org/arend/lib/pattern/ArendPattern.java 62 meta/src/main/java/org/arend/lib/pattern/PatternUtils.java 418 meta/src/main/java/org/arend/lib/ring/BigRational.java 35 meta/src/main/java/org/arend/lib/ring/IntRing.java 26 meta/src/main/java/org/arend/lib/ring/Monomial.java 88 meta/src/main/java/org/arend/lib/ring/Ring.java 7 meta/src/main/java/org/arend/lib/util/CountingSort.java 28 meta/src/main/java/org/arend/lib/util/DefImplInstanceSearchParameters.java 67 meta/src/main/java/org/arend/lib/util/Lazy.java 15 meta/src/main/java/org/arend/lib/util/Maybe.java 19 meta/src/main/java/org/arend/lib/util/NamedParameter.java 142 meta/src/main/java/org/arend/lib/util/RelationData.java 42 meta/src/main/java/org/arend/lib/util/Utils.java 435 meta/src/main/java/org/arend/lib/util/Values.java 42 meta/src/main/java/org/arend/lib/util/algorithms/ComMonoidWP.java 112 meta/src/main/java/org/arend/lib/util/algorithms/groebner/Buchberger.java 67 meta/src/main/java/org/arend/lib/util/algorithms/groebner/GroebnerBasisAlgorithm.java 8 meta/src/main/java/org/arend/lib/util/algorithms/idealmem/GroebnerIM.java 30 meta/src/main/java/org/arend/lib/util/algorithms/idealmem/IdealMembership.java 7 meta/src/main/java/org/arend/lib/util/algorithms/polynomials/DegLexMonomialOrder.java 15 meta/src/main/java/org/arend/lib/util/algorithms/polynomials/Monomial.java 106 meta/src/main/java/org/arend/lib/util/algorithms/polynomials/Poly.java 130 meta/src/main/java/org/arend/lib/util/algorithms/polynomials/Ring.java 50