norm_det simproc and eval_det tactic

A tactic for normalizing matrix determinants.

def normalizeBirdDet (e : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

reify a BirdDet call and normalize it using the certificate-chain evaluator

Equations

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

def norm_det : Lean.Meta.Simp.Simproc

Normalize a literal birdDet call using the certificate-chain evaluator.

Equations

• norm_det e = do let __do_lift ← liftM (normalizeBirdDet e) pure (Lean.Meta.Simp.Step.done __do_lift)

def evalDet : Lean.ParserDescr

Normalize birdDet calls in the target using the certificate-chain simproc.

Equations

• evalDet = Lean.ParserDescr.node `evalDet 1024 (Lean.ParserDescr.nonReservedSymbol "eval_det" false)