kdrag.theories.sexp.Unquote

kdrag.theories.sexp.Unquote(sexp: ExprRef) → tuple[ExprRef, Proof, Proof]

Interpret an s-expression as an expression.

>>> x = smt.Int("x")
>>> q, hi1, i1 = Quote(x + 1)
>>> e, hi2, i2 = Unquote(q)
>>> e
x + 1
>>> assert hi1.thm.eq(hi2.thm) and i1.thm.eq(i2.thm)