pub fn print_term_in(term: &Term, locals: &[&str]) -> Result<String, PrintError>Expand description
Spell term read in a context whose locals are locals: each prints as its own name. A goal and
its hypotheses are spelled this way for a reader; a closed term’s round trip is print_term’s,
which refuses a free name because the surface would read it as a global.