HomeIsabelle/Phabricator

Add PointerEq as a binary operation and reserve WordComparison for the tagged…

Description

Add PointerEq as a binary operation and reserve WordComparison for the tagged cases.
This avoids the problems with indexed cases with either arbitrary precision or
with datatypes with nullary constructors and one non-nullary constructor.

Details

Provenance
dcjmAuthored on Jul 6 2020, 6:23 PM
Parents
rPOLYMLfb10196d998b: Convert single bindings from mutual recursion into simple bindings.
Branches
Unknown
Tags
Unknown