Ah, that sounds like a pretty neat solution.
How exactly do I make ATS know that my function that does the or-ing should
make use of that proof?
d4v3y_5c0n3s schrieb am Samstag, 29. Mai 2021 um 15:39:37 UTC:
> 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/d55d521b-0a8b-4062-950b-40b315f9ed85n%40googlegroups.com.
