rzk-0.11.4: test/typecheck/cases/ill-kind-define-tope.rzk
#lang rzk-1 -- A definition at type U must define a type; a universe-kind body would be -- a synonym smuggling the kind into every position that accepts U. #define A : U := TOPE
#lang rzk-1 -- A definition at type U must define a type; a universe-kind body would be -- a synonym smuggling the kind into every position that accepts U. #define A : U := TOPE