Stream: General

Topic: temp Adding a size_definition to the termination solve

view this post on Zulip irvin (Dec 17 2025 at 11:32):

Is there a way to temporarily add a size_definition to the termination solver. The following allows lexicographic_order to prove termination of a function I have automatically but creates a permanent change.

instantiation bool :: size
begin

definition size_bool where [simp, code]: "size b = (if b then 1 else 0)"

instance ..

end

size_change also manages to prove without this type_class instantiation but it's slower.

Last updated: Dec 28 2025 at 02:03 UTC