rzk-0.11.4: test/typecheck/cases/ill-data-no-sharp-eliminator.rzk

#lang rzk-1

-- A #data generates no ♯ eliminators (see ill-match-modal-sharp).
#data Bool := false | true

#define retract : (z :_# Bool) -> Bool := rec-sharp-Bool Bool false true