Type Definition cop::offset::OTerm

type OTerm<'t, C> = Offset<&'t Term<C, usize>>;

Implementations

impl<'t, C> OTerm<'t, C>

pub fn whnf(self, sub: &Sub<'t, C>) -> Self

Substitute the head of the term until a fix point is reached.

let mut sub: Sub<&str> = Sub::default();
sub.set_dom_max(3);

let tm0: Term<&str, _> = Term::V(0);
let tm1: Term<&str, _> = Term::V(1);
let ot0 = OTerm::new(2, &tm0);
let ot1 = OTerm::new(0, &tm1);
sub.insert(2, ot1);

// 0+2 should be substituted to 1+0 and terminate there
assert!(ot0.whnf(&sub).ptr_eq(ot1))

Trait Implementations

impl<'t, C: Display> Display for OTerm<'t, C>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.