Expressive power of LH

[Kishlaya Jaiswal]

I know that we can create some new amazing types in LH, particularly, express some non-trivial subsets of Integers. For example:

{-@ type Nat = {v:Int | v>=0 } @-}
{-@ type grtN N = {v:Int | v>N } @-}
{-@ type Even = {v:Int | v mod 2 == 0 } @-}

But now what other non-trivial subsets can I express in LH? 

Can I create a type in LH which consists of only powers of 2? 

I tried doing that the following way but seems like it doesn't work.

(PS: If someone can answer the above question more precisely on SO, then it would be really helpful)

So a natural question which arises is what kind of subsets (of Integers) can I express?

Is there a nice characterization?

[Ranjit Jhala]

Hi Kishlaya

I replied to this on SO -- LMK if the answer doesn't make sense!

https://stackoverflow.com/questions/58806748/how-to-write-a-log2-function-in-liquid-haskell/58844705#58844705

- Ranjit.

--
You received this message because you are subscribed to the Google Groups "liquidhaskell" group.
To unsubscribe from this group and stop receiving emails from it, send an email to liquidhaskel...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/liquidhaskell/24d3e3b2-21fd-4c07-b6db-b19cc345b1d0%40googlegroups.com.