Function candidate_definition 

pub fn candidate_definition(
    ctx: &Context,
    name: &str,
    levels: Option<&[String]>,
    ty: &Term,
    body: &Term,
) -> Declaration

The definition a door of ctx puts to the core: its terms as ctx stores them (Context::stored_term) and the telescope the door gives it, the stated one or the level variables of the stored type and then of the body (term’s rules 1 and 4).