rzk-0.11.0: test/typecheck/cases/ill-lattice-ops-lub-unconditional.rzk
#lang rzk-1 -- From unrestricted t alone, sup s u <= t is not entailed (local context is ⊤). #define lubUnconditional (s u t : 2) (f : (x : 2 | sup s u <= x) -> U) : U := f t
#lang rzk-1 -- From unrestricted t alone, sup s u <= t is not entailed (local context is ⊤). #define lubUnconditional (s u t : 2) (f : (x : 2 | sup s u <= x) -> U) : U := f t