Function candidate_axiom 

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

The axiom a door of ctx puts to the core, its type stored and its levels read as candidate_definition reads them.