# Re: [isabelle] Declaring equal for a type; BNF not working on the left

Dear Gottfried,

`You cannot define equality in Isabelle/HOL for any type as you wish, as the HOL axioms
``already define it for all types. The datatype package (and the BNF package) introduce an
``algebraic type whose constructors are free, i.e., injective and their ranges pairwise
``distinct. If you want to have a coarser notion of equality, you can define your own
``function such as mTeq with fancy notation such as (infix "==="), but you cannot use HOL
``equality = for it, and the proof tools (esp. the simplifier) will not treat it as equality
``either.
`

`If you really want a type with your custom equality relation, you have to quotient your
``datatype through your custom equality relation [1] or directly construct a type with
``non-free type constructors [2]. You find more information on that in the references, but I
``have not examined your use case to see which route seems easier or feasible.
`
Andreas
[1] http://www21.in.tum.de/~kuncar/documents/huffman-kuncar-cpp2013.pdf

`[2]
``https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-August/004413.html
`

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*