rzk-0.9.0: test/typecheck/cases/ill-modal-sharp-bot-not-bot.rzk
#lang rzk-1 -- #BOT should not entail BOT: sharp tope is not accessible in plain context #def sharp-bot-not-bot (A : U) : (t : 2 | _# BOT) -> A := \ _ -> recBOT
#lang rzk-1 -- #BOT should not entail BOT: sharp tope is not accessible in plain context #def sharp-bot-not-bot (A : U) : (t : 2 | _# BOT) -> A := \ _ -> recBOT