[][src]Function term_rewriting::parse

pub fn parse(
    sig: &mut Signature,
    input: &str
) -> Result<(TRS, Vec<Term>), ParseError>

Parse a string as a TRS and a list of Terms.

let inp = "
#-- rules:
    S x_ y_ z_ = x_ z_ (y_ z_);
    K x_ y_ = x_;
    PLUS(SUCC(x_) y_) = PLUS(x_ SUCC(y_));
    PLUS(ZERO y_) = y_;

#-- terms:
    S K S K;
    PLUS(SUCC(SUCC(SUCC(ZERO))) SUCC(ZERO));
";
let (trs, terms) = parse(&mut Signature::default(), inp).unwrap();