Hey David, have you tried using the "praxi" syntax? It allows you to
define an axiom, essentially telling ATS: "I'm not going to prove that X is
true, but just assume it is." I'd recommend reading the theorem proving
sections of Intro to ATS if you haven't already.
Here's an example of a praxi that should suit your needs:
sortdef invals = {iv:int | iv < 0x20}
praxi lor_assumption {a,b,c:invals}{r:int} (
a:int a, b:int b, c:int c,
result: int r
) : [r < 0x8000] void
If you'd like me to explain what I'm doing here, just ask me and I can tell
you how this works. (By the way, I tested and this code compiles.)
On Sunday, May 23, 2021 at 7:22:52 PM UTC-4 gmhwxi wrote:
> This kind of guarantee can always be established with a run-time check.
>
> If you want to solve constraints involving 'lor', then you need to use an
> external solver like Z3.
> But it would require a lot of effort.
>
> I would suggest using a run-time check for now. And you could always come
> back to fix it later
> if really needed.
>
> On Sun, May 23, 2021 at 6:28 PM David Smith <sodab...@gmail.com> wrote:
>
>>
>> Hey, I have a small convenience function that takes 3 5 bit bit numbers
>> to produce a 15 bit color, that's guaranteed to be <0x8000.
>>
>> Now, apparently the typechecker doesn't know much about `lor`. Is there
>> any way I could say "hey trust me, if these three numbers are < 0x20 then
>> the result is < 0x8000"?
>>
>> Thanks in advance.
>>
>> --
>>
> You received this message because you are subscribed to the Google Groups
>> "ats-lang-users" group.
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to ats-lang-user...@googlegroups.com.
>> To view this discussion on the web visit
>> https://groups.google.com/d/msgid/ats-lang-users/4f5589ed-b80d-4662-918c-ac1fa81d04c9n%40googlegroups.com
>>
>> <https://groups.google.com/d/msgid/ats-lang-users/4f5589ed-b80d-4662-918c-ac1fa81d04c9n%40googlegroups.com?utm_medium=email&utm_source=footer>
>> .
>>
>
--
You received this message because you are subscribed to the Google Groups
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to ats-lang-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/f4a64ead-e20c-4389-a5d2-dbad4f7d8254n%40googlegroups.com.
