pub fn level_telescope(ctx: &Context, name: &str) -> Option<(Vec<String>, Term)>Expand description
A global’s universe parameters and type: its explicit level telescope, or else the level
variables its type mentions, which the Term kernel reads as bound by the declaration.