kdrag.rewrite.beta
- kdrag.rewrite.beta(e)
Do one pass of beta normalization.
>>> x = smt.Int("x") >>> y = smt.String("y") >>> f = smt.Function("f", smt.IntSort(), smt.IntSort()) >>> beta(f(x)) f(x) >>> beta(f(smt.Lambda([x], f(x))[1])) f(f(1)) >>> beta(f(smt.Select(smt.Lambda([x,y], x), 1, smt.StringVal("fred")))) f(1)