Reification support for the determinant tactic

This file contains the meta-level parser, refiyBirdDet, used by normalizeBirdDet to turn BirdDet.birdDet calls into the context used by the certificate-chain evaluator.

Main definitions

• reifyBirdDet: Parse a call to BirdDet.birdDet.

@[reducible, inline]

abbrev Mathlib.Tactic.Determinant.commSemiringOfCommRing {u : Lean.Level} {α : Q(Type u)} (rα : Q(CommRing «$α»)) : Q(CommSemiring «$α»)

Construct a CommSemiring instance expression from a CommRing instance expression

Equations

• Mathlib.Tactic.Determinant.commSemiringOfCommRing rα = q(CommRing.toCommSemiring)

def Mathlib.Tactic.Determinant.arrayLiteral? (e : Lean.Expr) : Lean.MetaM (Option (Array Lean.Expr))

Parse an array literal into an array of element expressions.

Compared to getArrayLit?, this also performs whnf.

Equations

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

structure Mathlib.Tactic.Determinant.Ctx {u : Lean.Level} {α : Q(Type u)} (rα : Q(CommRing «$α»)) : Type

The context for a certificate evaluation.

• cα : Ring.Common.Cache (commSemiringOfCommRing rα)

  Ring evaluation cache for the scalar ring.

• rc : Ring.Common.RingCompute Ring.RatCoeff (commSemiringOfCommRing rα)

  Proof-producing ring arithmetic.

• dimension : ℕ

  The dimension of the reified matrix

• dimensionLit : Q(ℕ)

  The quoted dimension expression from the reified determinant call.

• arrayExpr : Q(Array «$α»)

  The array of matrix entries as an Expr

• arrayEntries : Array Q(«$α»)

  An array of matrix entry Exprs`

structure Mathlib.Tactic.Determinant.ReifiedBirdDet : Type

The ring instance and evaluator context parsed by reifyBirdDet.

• u : Lean.Level

  The universe level associated with the birdDet call

• α : Q(Type udummy._uniq.14)

  The type of a matrix entry

• rα : Q(CommRing unknown_1)

  The CommRing instance for matrix entries

• ctx : Ctx self.rα

  The evaluator context for the parsed determinant expression.

def Mathlib.Tactic.Determinant.reifyBirdDet (e : Lean.Expr) : Lean.MetaM ReifiedBirdDet

Recognise a birdDet call and reify it into an evaluator context.

Equations

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