Universals/predicates in absview declaration

[Shea Levy]

Hi all,

Currently, my 'filedes' view is declared:

> absview filedes (fd: int)

Really, though, a valid file descriptor has to be a nat. If I try

> absview filedes (fd: nat)

compliation fails with

> the identifier [nat] is expected to refer to a sort (instead of a subset sort)

and all attempts to spell out a universal like

> absview filedes {n: nat} (fd: int n)

fail to parse. Is it possible to constrain an absview in this way?

~Shea

[gmhwxi]

>> Really, though, a valid file descriptor has to be a nat.

This piece of knowledge can be encoded in a lemma:

prfun lemma_filedes_param {n:int} (pf: !filedes(n)): [n >= 0] void

When you need the knowledge in your reasoning, you can do

prval () = lemma_filedes_param (pf) // assume [pf] is available at this point

[Shea Levy]

Ah I see, thanks!

~Shea

> --
> 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 post to this group, send email to ats-lan...@googlegroups.com.
> Visit this group at http://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/a5bf98ac-a353-4472-a300-30bf1d5847da%40googlegroups.com.