DelayedExpr — Mathlib

Lean4
/-- For proof terms generated by AC congruence closure modules, we want a placeholder as an equality
  proof between given two terms which will be generated by non-AC congruence closure modules later.
  `DelayedExpr` represents it using `eqProof`. -/
inductive DelayedExpr where/-- A `DelayedExpr` of just an `Expr`. -/

  | ofExpr (e : Expr) : DelayedExpr/--
A placeholder as an equality proof between given two terms which will be generated by non-AC
  congruence closure modules later. -/

  | eqProof (lhs rhs : Expr) : DelayedExpr/-- Will be applied to `congr_arg`. -/

  | congrArg (f : Expr) (h : DelayedExpr) : DelayedExpr/-- Will be applied to `congr_fun`. -/

  | congrFun (h : DelayedExpr) (a : ACApps) : DelayedExpr/-- Will be applied to `Eq.symm`. -/

  | eqSymm (h : DelayedExpr) : DelayedExpr/-- Will be applied to `Eq.symm`. -/

  | eqSymmOpt (a₁ a₂ : ACApps) (h : DelayedExpr) : DelayedExpr/-- Will be applied to `Eq.trans`. -/

  | eqTrans (h₁ h₂ : DelayedExpr) : DelayedExpr/-- Will be applied to `Eq.trans`. -/

  | eqTransOpt (a₁ a₂ a₃ : ACApps) (h₁ h₂ : DelayedExpr) : DelayedExpr/-- Will be applied to `heq_of_eq`. -/

  | heqOfEq (h : DelayedExpr) : DelayedExpr/-- Will be applied to `HEq.symm`. -/

  | heqSymm (h : DelayedExpr) : DelayedExpr
  deriving Inhabited
Похожие утверждения