pub fn reference_type(export: &str, declaration: &str) -> Result<Term, Verdict>Expand description
The type of declaration as the reference translator reads it from export.
declaration is either the Lean name (T06_002.transport) or its kernel spelling
(/s:"T06_002"/s:"transport").