Skip to content

Porting note: removed @[pp_nodot] #11180

Closed
Closed
Porting note: removed @[pp_nodot]#11180
Labels
porting-notesMathlib3 to Mathlib4 porting notes.
@pitmonticone

Description

@pitmonticone
pitmonticone
opened on Mar 5, 2024

Classifies porting notes claiming:

removed @[pp_nodot]

Examples

mathlib4/Mathlib/Algebra/Symmetrized.lean

Lines 48 to 57 in 2a65c8d

/-- The element of `SymAlg α` that represents `a : α`. -/
@[match_pattern]
-- Porting note: removed @[pp_nodot]
def sym : α ≃ αˢʸᵐ :=
Equiv.refl _
#align sym_alg.sym SymAlg.sym
/-- The element of `α` represented by `x : αˢʸᵐ`. -/
-- Porting note: removed @[pp_nodot]
def unsym : αˢʸᵐ ≃ α :=

Metadata

Metadata

Assignees

No one assigned

    Labels

    porting-notesMathlib3 to Mathlib4 porting notes.

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions