Lean4
/-- The core function for `monoidal` and `bicategory` tactics. -/
def main (ρ : Type) [Context ρ] [MonadMor₁ (CoherenceM ρ)] [MonadMor₂Iso (CoherenceM ρ)]
[MonadNormalExpr (CoherenceM ρ)] [MkEval (CoherenceM ρ)] [MkMor₂ (CoherenceM ρ)] [MonadMor₂ (CoherenceM ρ)]
[MonadCoherehnceHom (CoherenceM ρ)] [MonadNormalizeNaturality (CoherenceM ρ)] [MkEqOfNaturality (CoherenceM ρ)]
(nm : Name) (mvarId : MVarId) : MetaM (List MVarId) :=
mvarId.withContext
(do
let mvarIds ← normalForm ρ nm mvarId
let (mvarIdsCoherence, mvarIdsRefl) := List.splitEvenOdd (← repeat' ofNormalizedEq mvarIds)
for mvarId in mvarIdsRefl do
mvarId.refl
let mvarIds'' ←
mvarIdsCoherence.mapM fun mvarId => do
withTraceNode nm
(fun _ => do
return m!"goal: {← mvarId.getType}")
(do
try
pureCoherence ρ nm mvarId
catch _ =>
return [mvarId])
return mvarIds''.flatten)
