653 | (Const (@{const_name of_nat}, T as @{typ "nat => int"}), []) => |
653 | (Const (@{const_name of_nat}, T as @{typ "nat => int"}), []) => |
654 Cst (NatToInt, T, Any) |
654 Cst (NatToInt, T, Any) |
655 | (Const (@{const_name of_nat}, |
655 | (Const (@{const_name of_nat}, |
656 T as @{typ "unsigned_bit word => signed_bit word"}), []) => |
656 T as @{typ "unsigned_bit word => signed_bit word"}), []) => |
657 Cst (NatToInt, T, Any) |
657 Cst (NatToInt, T, Any) |
658 | (Const (@{const_name lower_semilattice_fun_inst.inf_fun}, T), |
658 | (Const (@{const_name semilattice_inf_fun_inst.inf_fun}, T), |
659 [t1, t2]) => |
659 [t1, t2]) => |
660 Op2 (Intersect, nth_range_type 2 T, Any, sub t1, sub t2) |
660 Op2 (Intersect, nth_range_type 2 T, Any, sub t1, sub t2) |
661 | (Const (@{const_name upper_semilattice_fun_inst.sup_fun}, T), |
661 | (Const (@{const_name semilattice_sup_fun_inst.sup_fun}, T), |
662 [t1, t2]) => |
662 [t1, t2]) => |
663 Op2 (Union, nth_range_type 2 T, Any, sub t1, sub t2) |
663 Op2 (Union, nth_range_type 2 T, Any, sub t1, sub t2) |
664 | (t0 as Const (@{const_name minus_fun_inst.minus_fun}, T), [t1, t2]) => |
664 | (t0 as Const (@{const_name minus_fun_inst.minus_fun}, T), [t1, t2]) => |
665 Op2 (SetDifference, nth_range_type 2 T, Any, sub t1, sub t2) |
665 Op2 (SetDifference, nth_range_type 2 T, Any, sub t1, sub t2) |
666 | (t0 as Const (@{const_name ord_fun_inst.less_eq_fun}, T), [t1, t2]) => |
666 | (t0 as Const (@{const_name ord_fun_inst.less_eq_fun}, T), [t1, t2]) => |