pub fn parse(
sig: &mut Signature,
input: &str
) -> Result<(TRS, Vec<Term>), ParseError>
Parse a string as a TRS
and a list of Term
s.
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();