Ruslan Shevchenko (Nov 04 2023 at 10:44): Ruslan Shevchenko (Nov 04 2023 at 10:44):Hi,
If I have a domain of functions where input is {1..n} and output is {1..m}, can I express this as type?
Mathias Fleury (Nov 04 2023 at 11:19):Can you express this as a type? Yes, this is similar to the setup for words in HOL-Library.Word
typedef (overloaded) 'a bound = "{n. n ≤ LENGTH('a::len0)}"
by auto
definition test :: ‹3 bound ⇒ 5 bound› where
‹test = undefined›
Should you do it? I do not think so. Typelifting and co is not really easy to use and very annoying. It will be a lot easier to have an precondition on the function.
Ruslan Shevchenko (Nov 04 2023 at 13:17):Thanks, will recheck.
Wolfgang Jeltsch (Nov 17 2023 at 15:17):Mathias Fleury said:
Can you express this as a type? Yes, this is similar to the setup for words in HOL-Library.Word
typedef (overloaded) 'a bound = "{n. n ≤ LENGTH('a::len0)}" by auto definition test :: ‹3 bound ⇒ 5 bound› where ‹test = undefined›Should you do it? I do not think so. Typelifting and co is not really easy to use and very annoying. It will be a lot easier to have an precondition on the function.
This is very interesting. I’ve never head of LENGTH and len0. Where is this introduced, and where is this documented? Is this about type-level natural numbers? Also, what is the difference between len0 and len, which the Word theory uses?
Mathias Fleury (Nov 17 2023 at 15:20):len0 is the same as len but non-zero
Mathias Fleury (Nov 17 2023 at 15:20):Mostly because words of length 0 are weird
Wolfgang Jeltsch (Nov 17 2023 at 15:23):I see. Is there any documentation of LENGTH, len, and len0 somewhere? At the moment, I’m not sure what these exactly are and how to use them.
Mathias Fleury (Nov 17 2023 at 15:36):I don't think that there is much besides the point where this is defined (https://www.isa-afp.org/browser_info/devel/HOL/HOL-Word/Type_Length.html)
Wolfgang Jeltsch (Nov 17 2023 at 16:11):Well, that’s certainly pretty illuminating.
Last updated: Oct 24 2025 at 01:37 UTC