(n: int)
| 36 | return Expr.const(mk_name(s), []) |
| 37 | |
| 38 | def mk_nat(n: int): |
| 39 | return Expr.app( |
| 40 | Expr.app( |
| 41 | Expr.app(mk_const("OfNat.ofNat"), mk_const("Nat")), |
| 42 | Expr.lit(Literal.natVal(n)), |
| 43 | ), |
| 44 | mk_const("inst"), |
| 45 | ) |
| 46 | |
| 47 | def mk_binop(op_name: str, a, b): |
| 48 | op = mk_const(op_name) |