Skip to main content

nf

Function nf 

Source
pub fn nf(term: &Node, env: &mut Env) -> Node
Expand description

Public full normal form API (issue #50, D4). Reduces every redex in term, including those nested under binders and in argument positions, until the term is in beta-(eta-)normal form. The result is post-processed by flatten_neutral_applies so it prints in the surface shape (succ (succ zero)) from the issue.