@[instance_reducible]

def HexRowReduceTheory.Tactic.instFieldRat_hexRowReduceTheory : Lean.Grind.Field ℚ

Equations

• HexRowReduceTheory.Tactic.instFieldRat_hexRowReduceTheory = Field.toGrindField

@[instance_reducible]

instance HexRowReduceTheory.Tactic.instToExprScaled_hexRowReduceTheory : Lean.ToExpr Hex.Matrix.Lists.Scaled

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.instToExprScaled_hexRowReduceTheory.toExpr : Hex.Matrix.Lists.Scaled → Lean.Expr

Equations

• HexRowReduceTheory.Tactic.instToExprScaled_hexRowReduceTheory.toExpr { denom := a, nums := a_1 } = ((Lean.Expr.const `Hex.Matrix.Lists.Scaled.mk []).app (Lean.toExpr a)).app (Lean.toExpr a_1)

@[instance_reducible]

instance HexRowReduceTheory.Tactic.instToExprScaledRows_hexRowReduceTheory : Lean.ToExpr Hex.Matrix.Lists.ScaledRows

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.instToExprScaledRows_hexRowReduceTheory.toExpr : Hex.Matrix.Lists.ScaledRows → Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.instToExprInverseWitness_hexRowReduceTheory.toExpr : Hex.Matrix.InverseWitness → Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance HexRowReduceTheory.Tactic.instToExprInverseWitness_hexRowReduceTheory : Lean.ToExpr Hex.Matrix.InverseWitness

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.instToExprSolveBasis_hexRowReduceTheory.toExpr : Hex.Matrix.SolveBasis → Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance HexRowReduceTheory.Tactic.instToExprSolveBasis_hexRowReduceTheory : Lean.ToExpr Hex.Matrix.SolveBasis

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance HexRowReduceTheory.Tactic.instToExprSolveWitness_hexRowReduceTheory : Lean.ToExpr Hex.Matrix.SolveWitness

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.instToExprSolveWitness_hexRowReduceTheory.toExpr : Hex.Matrix.SolveWitness → Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

inductive HexRowReduceTheory.Tactic.Outcome (α : Type) : Type

• notApplicable {α : Type} : Outcome α
• declined {α : Type} (message : Lean.MessageData) : Outcome α
• success {α : Type} (value : α) : Outcome α

structure HexRowReduceTheory.Tactic.Input : Type

• literal : HexMatrixTheory.Literal.Recognized
• rows : List (List ℚ)

structure HexRowReduceTheory.Tactic.VecInput : Type

• literal : HexMatrixTheory.Literal.VectorLiteral
• entries : List ℚ

def HexRowReduceTheory.Tactic.matrixLiteral? (A : Lean.Expr) (n m : ℕ) : Lean.MetaM (Option HexMatrixTheory.Literal.Recognized)

Constant zero and identity matrices use the shared closed-function route.

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.readMatrix (A : Lean.Expr) : Lean.MetaM (Outcome Input)

Rational matrix recognition, with shared literal identification.

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.closedVector? (v : Lean.Expr) : Lean.MetaM (Option HexMatrixTheory.Literal.VectorLiteral)

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.readVector (v : Lean.Expr) : Lean.MetaM (Outcome VecInput)

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.inputMatrix (c : Input) : Hex.Matrix ℚ c.literal.n c.literal.m

Equations

• HexRowReduceTheory.Tactic.inputMatrix c = Hex.Matrix.ofFn fun (i : Fin c.literal.n) (j : Fin c.literal.m) => (Array.map List.toArray c.rows.toArray)[↑i]![↑j]!

def HexRowReduceTheory.Tactic.inputVector (c : VecInput) : Vector ℚ c.literal.size

Equations

• HexRowReduceTheory.Tactic.inputVector c = Vector.ofFn fun (i : Fin c.literal.size) => c.entries.toArray[↑i]!

def HexRowReduceTheory.Tactic.truth (check : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.positive (n : ℕ) : Lean.MetaM Lean.Expr

Equations

• HexRowReduceTheory.Tactic.positive n = do let __do_lift ← Lean.Meta.mkAppM `LT.lt #[Lean.mkNatLit 0, Lean.mkNatLit n] HexMatrixTheory.Literal.decideProof __do_lift

def HexRowReduceTheory.Tactic.checked (operation : String) (target proof : Lean.Expr) : Lean.MetaM Lean.Expr

One synchronous kernel declaration, without a preliminary type check.

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.andLeft (h : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

• HexRowReduceTheory.Tactic.andLeft h = Lean.Meta.mkAppM `And.left #[h]

def HexRowReduceTheory.Tactic.andRight (h : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

• HexRowReduceTheory.Tactic.andRight h = Lean.Meta.mkAppM `And.right #[h]

def HexRowReduceTheory.Tactic.identifyMatrix (A : Lean.Expr) (c : Input) (s : Hex.Matrix.Lists.ScaledRows) : Lean.MetaM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.identifyVector (v : Lean.Expr) (c : VecInput) (s : Hex.Matrix.Lists.Scaled) : Lean.MetaM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.matrixLiteral (n m : ℕ) (s : Hex.Matrix.Lists.ScaledRows) : Lean.MetaM (Lean.Expr × Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.vectorLiteral (n : ℕ) (s : Hex.Matrix.Lists.Scaled) : Lean.MetaM (Lean.Expr × Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.inputHeights (rows : List (List ℚ)) (input : Hex.Matrix.Lists.ScaledRows) : List (String × Lean.Json)

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.reportInverse (c : Input) (w : Hex.Matrix.InverseWitness) : Lean.MetaM Unit

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.reportSolve (c : Input) (b : VecInput) (w : Hex.Matrix.SolveWitness) : Lean.MetaM Unit

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.inverseWitness (c : Input) : Lean.MetaM Hex.Matrix.InverseWitness

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.solveWitness (c : Input) (b : VecInput) : Lean.MetaM Hex.Matrix.SolveWitness

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.inverseProof (A : Lean.Expr) (c : Input) (w : Hex.Matrix.InverseWitness) : Lean.MetaM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.solveProof (A b : Lean.Expr) (c : Input) (rhs : VecInput) (w : Hex.Matrix.SolveWitness) : Lean.MetaM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.inverseResult (A : Lean.Expr) (c : Input) (w : Hex.Matrix.InverseWitness) : Lean.MetaM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.solveResult (A b : Lean.Expr) (c : Input) (rhs : VecInput) (w : Hex.Matrix.SolveWitness) : Lean.MetaM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.inverseGoal (target : Lean.Expr) : Lean.MetaM (Outcome Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.

structure HexRowReduceTheory.Tactic.SolveGoal : Type

The equation inside either an ordinary or existential solve goal.

• matrix : Lean.Expr
• rhs : Lean.Expr
• candidate : Option Lean.Expr
• reversed : Bool
• negative : Bool

def HexRowReduceTheory.Tactic.matchSolve? (target : Lean.Expr) : Lean.MetaM (Option SolveGoal)

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.solveGoal (target : Lean.Expr) : Lean.MetaM (Outcome Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.inverseTerm : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.solveTerm : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.inverseTermFallback : Lean.Elab.Term.TermElab

Equations

• HexRowReduceTheory.Tactic.inverseTermFallback x✝¹ x✝ = Lean.throwError (Lean.toMessageData "inverse: not applicable: expected a closed square rational matrix")

def HexRowReduceTheory.Tactic.elabInverseTerm : Lean.Elab.Term.TermElab

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.solveTermFallback : Lean.Elab.Term.TermElab

Equations

• HexRowReduceTheory.Tactic.solveTermFallback x✝¹ x✝ = Lean.throwError (Lean.toMessageData "solve: not applicable: expected a closed rational matrix and vector")

def HexRowReduceTheory.Tactic.elabSolveTerm : Lean.Elab.Term.TermElab

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.inverseTac : Lean.ParserDescr

Equations

• HexRowReduceTheory.Tactic.inverseTac = Lean.ParserDescr.node `HexRowReduceTheory.Tactic.inverseTac 1022 (Lean.ParserDescr.nonReservedSymbol "inverse" false)

def HexRowReduceTheory.Tactic.solveTac : Lean.ParserDescr

Equations

• HexRowReduceTheory.Tactic.solveTac = Lean.ParserDescr.node `HexRowReduceTheory.Tactic.solveTac 1022 (Lean.ParserDescr.nonReservedSymbol "solve" false)

def HexRowReduceTheory.Tactic.inverseFallback : Lean.Elab.Tactic.Tactic

Equations

• HexRowReduceTheory.Tactic.inverseFallback x✝ = Lean.throwError (Lean.toMessageData "inverse: not applicable: expected A * B = 1 or A⁻¹ = B over ℚ, in either orientation")

def HexRowReduceTheory.Tactic.evalInverse : Lean.Elab.Tactic.Tactic

Equations

• One or more equations did not get rendered due to their size.

def HexRowReduceTheory.Tactic.solveFallback : Lean.Elab.Tactic.Tactic

Equations

• HexRowReduceTheory.Tactic.solveFallback x✝ = Lean.throwError (Lean.toMessageData "solve: not applicable: expected a rational mulVec equation, existence, or nonexistence")

def HexRowReduceTheory.Tactic.evalSolve : Lean.Elab.Tactic.Tactic

Equations

• One or more equations did not get rendered due to their size.