How to turn Integer into Proxy (n :: KnownNat) with n equal to the integer?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

How to turn Integer into Proxy (n :: KnownNat) with n equal to the integer?

David Banas-2
I’d like to use Data.Vector.Sized.slice’, but it wants the starting position and length parameters as Proxys, not Integers.
How can I convert an Integer into a Proxy (n :: KnownNat) with n equal to the integer?

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: How to turn Integer into Proxy (n :: KnownNat) with n equal to the integer?

David Kraeutmann

The best you can do is `someNatVal`:

case someNatVal 10 of
  Just (SomeNat p) -> _ {- do stuff with p -}
  _ -> _ {- not a nat -}

On 8/3/2018 11:01 PM, David Banas wrote:
I’d like to use Data.Vector.Sized.slice’, but it wants the starting position and length parameters as Proxys, not Integers.
How can I convert an Integer into a Proxy (n :: KnownNat) with n equal to the integer?

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.