Equations
- Regex.Data.instReprAnchor = { reprPrec := Regex.Data.instReprAnchor.repr }
Equations
- One or more equations did not get rendered due to their size.
- Regex.Data.instReprAnchor.repr Regex.Data.Anchor.start prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Regex.Data.Anchor.start")).group prec✝
- Regex.Data.instReprAnchor.repr Regex.Data.Anchor.eos prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Regex.Data.Anchor.eos")).group prec✝
Instances For
Instances For
Equations
Equations
- Regex.Data.instToExprAnchor = { toExpr := Regex.Data.instToExprAnchor.toExpr✝, toTypeExpr := Lean.Expr.const `Regex.Data.Anchor [] }