# Declaring an external view prval

**URL:** <https://discourse.ats-lang.org/t/declaring-an-external-view-prval/271>\
**Category:** Google Group\
**Created:** [August 30, 2014, 11:31pm UTC](https://discourse.ats-lang.org/t/declaring-an-external-view-prval/271 "2014-08-30T23:31:49Z")\
**Posts on this page:** 9\
**Page:** 1

<div class="post-metadata">

**Author:** ![Shea\_Levy](https://avatars.discourse-cdn.com/v4/letter/s/b38774/32.png) [@Shea\_Levy](https://discourse.ats-lang.org/u/Shea_Levy)\
**Post date:** [August 30, 2014, 11:31pm UTC](https://discourse.ats-lang.org/t/declaring-an-external-view-prval/271/1 "2014-08-30T23:31:49Z")

</div>

Hi all,

I have an abstract view ‘filedes’ parameterized by an int file  
descriptor. I want to declare that, at the beginning of the program,  
stderr is an open file, so I have this line in fd.sats:

> prval stderr\_fileno\_pf : filedes(2)

Typechecking fails with

> the static expression is of the sort [S2RTbas(S2RTBASimp(7; view))] but it is expectecd to be of the sort [S2RTbas(S2RTBASimp(5; prop))]

which is clear enough, but if prval is not the right way to go how do I  
declare a view proof value?

~Shea

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [August 31, 2014, 2:56am UTC](https://discourse.ats-lang.org/t/declaring-an-external-view-prval/271/2 "2014-08-31T02:56:25Z")

</div>

First,

%{# should be changed to %{^

%{# should only be used in a SATS file.

You code should look like this:

%{^ #include “include/common.h” %}  
staload “static/fd.sats” //  
// staload “dynamic/fd.dats” //  
implement main () = let  
prval pf = make () where  
{  
extern make (): filedes(2)  
}  
val \_ = close(stderr\_fileno\_pf | 2) in 0 endOn Saturday, August 30, 2014 10:44:03 PM UTC-4, Shea Levy wrote:

> Ah, I see. I’m now stuck at an error I don’t understand. My code is at  
> [1](https://github.com/shlevy/socket-activate/blob/WIP/dynamic/socket-activate.dats), [2](https://github.com/shlevy/socket-activate/blob/WIP/static/fd.sats), and [3](https://github.com/shlevy/socket-activate/blob/WIP/dynamic/fd.dats), and the errors I get are:
> 
> > /home/shlevy/src/socket-activate/dynamic/socket-activate.dats:  
> > 129(line=9, offs=17) – 145(line=9, offs=33): error(3): the linear dynamic  
> > variable [stderr\_fileno\_pf$63(-1)] is expected to be local but it is not.  
> > /home/shlevy/src/socket-activate/dynamic/socket-activate.dats:  
> > 129(line=9, offs=17) – 145(line=9, offs=33): error(3):  
> > [/home/hwxi/research/Postiats/git/src/pats\_trans3\_util.dats]: d3exp\_trdn:  
> > the dynamic expression cannot be assigned the type [S2Eapp(S2Ecst(filedes); S2EVar(1))].  
> > /home/shlevy/src/socket-activate/dynamic/socket-activate.dats:  
> > 129(line=9, offs=17) – 145(line=9, offs=33): error(3): mismatch of static  
> > terms (tyleq):  
> > The actual term is: S2Eapp(S2Ecst(filedes\_impl); S2Eintinf(2))  
> > The needed term is: S2Eapp(S2Ecst(filedes); S2EVar(1))
> 
> I’m afraid I’m lost for both of these. Why is the proof expected to be  
> local? And why is filedes\_impl being exposed?
> 
> ~Shea
> 
> On Sat, Aug 30, 2014 at 10:09:11PM -0400, Hongwei Xi wrote:
> 
> > The code should be in a DATS file.
> > 
> > On Sat, Aug 30, 2014 at 10:06 PM, Shea Levy \<[sh...@shealevy.com](mailto:sh...@shealevy.com) \<javascript:\>\> wrote:
> > 
> > > Hm, this fails with
> > > 
> > > > error(parsing): the syntactic entity [colonwith] is needed.
> > > 
> > > ~Shea
> > > 
> > > On Sat, Aug 30, 2014 at 06:16:13PM -0700, gmhwxi wrote:
> > > 
> > > > If I understand your situation correctly, I would do something like  
> > > > this:
> > > > 
> > > > prval  
> > > > stderr\_fileno\_pf = \_\_assert () where  
> > > > {  
> > > > extern praxi \_\_assert (): filedes(2)  
> > > > }
> > > > 
> > > > On Saturday, August 30, 2014 7:31:53 PM UTC-4, Shea Levy wrote:
> > > > 
> > > > > Hi all,
> > > > > 
> > > > > I have an abstract view ‘filedes’ parameterized by an int file  
> > > > > descriptor. I want to declare that, at the beginning of the  
> > > > > program,  
> > > > > stderr is an open file, so I have this line in fd.sats:
> > > > > 
> > > > > > prval stderr\_fileno\_pf : filedes(2)
> > > > > 
> > > > > Typechecking fails with
> > > > > 
> > > > > > the static expression is of the sort [S2RTbas(S2RTBASimp(7; view))]  
> > > > > > but  
> > > > > > it is expectecd to be of the sort [S2RTbas(S2RTBASimp(5; prop))]
> > > > > 
> > > > > which is clear enough, but if prval is not the right way to go how  
> > > > > do I  
> > > > > declare a view proof value?
> > > > > 
> > > > > ~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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > > > \<javascript:\>.  
> > > > Visit this group at [http://groups.google.com/group/ats-lang-users](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/e05c4c07-2cc3-4586-8d12-22f818f5043f%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/e05c4c07-2cc3-4586-8d12-22f818f5043f%40googlegroups.com)
> 
> > > .
> > > 
> > > –  
> > > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > > \<javascript:\>.  
> > > Visit this group at [http://groups.google.com/group/ats-lang-users](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/20140831020626.GD7772%40nixos.hsd1.nh.comcast.net](https://groups.google.com/d/msgid/ats-lang-users/20140831020626.GD7772%40nixos.hsd1.nh.comcast.net)
> 
> > > .
> > 
> > –  
> > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > \<javascript:\>.  
> > Visit this group at [http://groups.google.com/group/ats-lang-users](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/CAPPSPLr4npLL9EzmQE3eEL4%3DG1EaPn%3DKfUDkdx86ukXVp%3DC8RA%40mail.gmail.com](https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLr4npLL9EzmQE3eEL4%3DG1EaPn%3DKfUDkdx86ukXVp%3DC8RA%40mail.gmail.com).

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [August 31, 2014, 3:09am UTC](https://discourse.ats-lang.org/t/declaring-an-external-view-prval/271/3 "2014-08-31T03:09:39Z")

</div>

A linear proof cannot be shared; it can only be borrowed.  
This is a complicated issue. For now, the shortcut I showed is  
probably the easiest way to take.On Saturday, August 30, 2014 11:01:29 PM UTC-4, Shea Levy wrote:

> Ah, I see, so is there no way to modularly declare a linear proof like  
> this? I have to have a praxi in every function that uses it?
> 
> On Sat, Aug 30, 2014 at 07:56:25PM -0700, gmhwxi wrote:
> 
> > First,
> > 
> > %{# should be changed to %{^
> > 
> > %{# should only be used in a SATS file.
> > 
> > You code should look like this:
> > 
> > %{^ #include “include/common.h” %}  
> > staload “static/fd.sats” //  
> > // staload “dynamic/fd.dats” //  
> > implement main () = let  
> > prval pf = make () where  
> > {  
> > extern make (): filedes(2)  
> > }  
> > val \_ = close(stderr\_fileno\_pf | 2) in 0 end
> > 
> > On Saturday, August 30, 2014 10:44:03 PM UTC-4, Shea Levy wrote:
> > 
> > > Ah, I see. I’m now stuck at an error I don’t understand. My code is at  
> > > [1], [2](https://github.com/shlevy/socket-activate/blob/WIP/static/fd.sats), and [3](https://github.com/shlevy/socket-activate/blob/WIP/dynamic/fd.dats), and the errors I get are:
> > > 
> > > > /home/shlevy/src/socket-activate/dynamic/socket-activate.dats:  
> > > > 129(line=9, offs=17) – 145(line=9, offs=33): error(3): the linear  
> > > > dynamic  
> > > > variable [stderr\_fileno\_pf$63(-1)] is expected to be local but it is  
> > > > not.  
> > > > /home/shlevy/src/socket-activate/dynamic/socket-activate.dats:  
> > > > 129(line=9, offs=17) – 145(line=9, offs=33): error(3):  
> > > > [/home/hwxi/research/Postiats/git/src/pats\_trans3\_util.dats]:  
> > > > d3exp\_trdn:  
> > > > the dynamic expression cannot be assigned the type  
> > > > [S2Eapp(S2Ecst(filedes); S2EVar(1))].  
> > > > /home/shlevy/src/socket-activate/dynamic/socket-activate.dats:  
> > > > 129(line=9, offs=17) – 145(line=9, offs=33): error(3): mismatch of  
> > > > static  
> > > > terms (tyleq):  
> > > > The actual term is: S2Eapp(S2Ecst(filedes\_impl); S2Eintinf(2))  
> > > > The needed term is: S2Eapp(S2Ecst(filedes); S2EVar(1))
> > > 
> > > I’m afraid I’m lost for both of these. Why is the proof expected to be  
> > > local? And why is filedes\_impl being exposed?
> > > 
> > > [1]:
> 
> [https://github.com/shlevy/socket-activate/blob/WIP/dynamic/socket-activate.dats](https://github.com/shlevy/socket-activate/blob/WIP/dynamic/socket-activate.dats)
> 
> > > ~Shea
> > > 
> > > On Sat, Aug 30, 2014 at 10:09:11PM -0400, Hongwei Xi wrote:
> > > 
> > > > The code should be in a DATS file.
> > > > 
> > > > On Sat, Aug 30, 2014 at 10:06 PM, Shea Levy \<[sh...@shealevy.com](mailto:sh...@shealevy.com) \<javascript:\>\> wrote:
> > > > 
> > > > > Hm, this fails with
> > > > > 
> > > > > > error(parsing): the syntactic entity [colonwith] is needed.
> > > > > 
> > > > > ~Shea
> > > > > 
> > > > > On Sat, Aug 30, 2014 at 06:16:13PM -0700, gmhwxi wrote:
> > > > > 
> > > > > > If I understand your situation correctly, I would do something  
> > > > > > like  
> > > > > > this:
> > > > > > 
> > > > > > prval  
> > > > > > stderr\_fileno\_pf = \_\_assert () where  
> > > > > > {  
> > > > > > extern praxi \_\_assert (): filedes(2)  
> > > > > > }
> > > > > > 
> > > > > > On Saturday, August 30, 2014 7:31:53 PM UTC-4, Shea Levy wrote:
> > > > > > 
> > > > > > > Hi all,
> > > > > > > 
> > > > > > > I have an abstract view ‘filedes’ parameterized by an int file  
> > > > > > > descriptor. I want to declare that, at the beginning of the  
> > > > > > > program,  
> > > > > > > stderr is an open file, so I have this line in fd.sats:
> > > > > > > 
> > > > > > > > prval stderr\_fileno\_pf : filedes(2)
> > > > > > > 
> > > > > > > Typechecking fails with
> > > > > > > 
> > > > > > > > the static expression is of the sort [S2RTbas(S2RTBASimp(7; view))]  
> > > > > > > > but  
> > > > > > > > it is expectecd to be of the sort [S2RTbas(S2RTBASimp(5; prop))]
> > > > > > > 
> > > > > > > which is clear enough, but if prval is not the right way to go  
> > > > > > > how  
> > > > > > > do I  
> > > > > > > declare a view proof value?
> > > > > > > 
> > > > > > > ~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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > > > > > \<javascript:\>.  
> > > > > > Visit this group at  
> > > > > > [http://groups.google.com/group/ats-lang-users](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/e05c4c07-2cc3-4586-8d12-22f818f5043f%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/e05c4c07-2cc3-4586-8d12-22f818f5043f%40googlegroups.com)
> 
> > > > > .
> > > > > 
> > > > > –  
> > > > > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > > > > \<javascript:\>.  
> > > > > Visit this group at [http://groups.google.com/group/ats-lang-users](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/20140831020626.GD7772%40nixos.hsd1.nh.comcast.net](https://groups.google.com/d/msgid/ats-lang-users/20140831020626.GD7772%40nixos.hsd1.nh.comcast.net)
> 
> > > > > .
> > > > 
> > > > –  
> > > > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > > > \<javascript:\>.  
> > > > Visit this group at [http://groups.google.com/group/ats-lang-users](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/CAPPSPLr4npLL9EzmQE3eEL4%3DG1EaPn%3DKfUDkdx86ukXVp%3DC8RA%40mail.gmail.com](https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLr4npLL9EzmQE3eEL4%3DG1EaPn%3DKfUDkdx86ukXVp%3DC8RA%40mail.gmail.com).
> 
> > > 
> > 
> > –  
> > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > \<javascript:\>.  
> > Visit this group at [http://groups.google.com/group/ats-lang-users](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/fb4aefb5-a045-4bf7-8163-9a950ed8b6bd%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/fb4aefb5-a045-4bf7-8163-9a950ed8b6bd%40googlegroups.com).

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [August 31, 2014, 2:09am UTC](https://discourse.ats-lang.org/t/declaring-an-external-view-prval/271/4 "2014-08-31T02:09:11Z")

</div>

The code should be in a DATS file.On Sat, Aug 30, 2014 at 10:06 PM, Shea Levy [sh...@shealevy.com](mailto:sh...@shealevy.com) wrote:

> Hm, this fails with
> 
> > error(parsing): the syntactic entity [colonwith] is needed.
> 
> ~Shea
> 
> On Sat, Aug 30, 2014 at 06:16:13PM -0700, gmhwxi wrote:
> 
> > If I understand your situation correctly, I would do something like this:
> > 
> > prval  
> > stderr\_fileno\_pf = \_\_assert () where  
> > {  
> > extern praxi \_\_assert (): filedes(2)  
> > }
> > 
> > On Saturday, August 30, 2014 7:31:53 PM UTC-4, Shea Levy wrote:
> > 
> > > Hi all,
> > > 
> > > I have an abstract view ‘filedes’ parameterized by an int file  
> > > descriptor. I want to declare that, at the beginning of the program,  
> > > stderr is an open file, so I have this line in fd.sats:
> > > 
> > > > prval stderr\_fileno\_pf : filedes(2)
> > > 
> > > Typechecking fails with
> > > 
> > > > the static expression is of the sort [S2RTbas(S2RTBASimp(7; view))]  
> > > > but  
> > > > it is expectecd to be of the sort [S2RTbas(S2RTBASimp(5; prop))]
> > > 
> > > which is clear enough, but if prval is not the right way to go how do I  
> > > declare a view proof value?
> > > 
> > > ~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](mailto:ats-lang-user...@googlegroups.com).  
> > To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> > Visit this group at [http://groups.google.com/group/ats-lang-users](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/e05c4c07-2cc3-4586-8d12-22f818f5043f%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/e05c4c07-2cc3-4586-8d12-22f818f5043f%40googlegroups.com)  
> > .
> 
> –  
> 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](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](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/20140831020626.GD7772%40nixos.hsd1.nh.comcast.net](https://groups.google.com/d/msgid/ats-lang-users/20140831020626.GD7772%40nixos.hsd1.nh.comcast.net)  
> .

---

<div class="post-metadata">

**Author:** ![Shea\_Levy](https://avatars.discourse-cdn.com/v4/letter/s/b38774/32.png) [@Shea\_Levy](https://discourse.ats-lang.org/u/Shea_Levy)\
**Post date:** [August 31, 2014, 2:44am UTC](https://discourse.ats-lang.org/t/declaring-an-external-view-prval/271/5 "2014-08-31T02:44:00Z")

</div>

Ah, I see. I’m now stuck at an error I don’t understand. My code is at  
[1](https://github.com/shlevy/socket-activate/blob/WIP/dynamic/socket-activate.dats), [2](https://github.com/shlevy/socket-activate/blob/WIP/static/fd.sats), and [3](https://github.com/shlevy/socket-activate/blob/WIP/dynamic/fd.dats), and the errors I get are:

> /home/shlevy/src/socket-activate/dynamic/socket-activate.dats: 129(line=9, offs=17) – 145(line=9, offs=33): error(3): the linear dynamic variable [stderr\_fileno\_pf$63(-1)] is expected to be local but it is not.  
> /home/shlevy/src/socket-activate/dynamic/socket-activate.dats: 129(line=9, offs=17) – 145(line=9, offs=33): error(3): [/home/hwxi/research/Postiats/git/src/pats\_trans3\_util.dats]: d3exp\_trdn: the dynamic expression cannot be assigned the type [S2Eapp(S2Ecst(filedes); S2EVar(1))].  
> /home/shlevy/src/socket-activate/dynamic/socket-activate.dats: 129(line=9, offs=17) – 145(line=9, offs=33): error(3): mismatch of static terms (tyleq):  
> The actual term is: S2Eapp(S2Ecst(filedes\_impl); S2Eintinf(2))  
> The needed term is: S2Eapp(S2Ecst(filedes); S2EVar(1))

I’m afraid I’m lost for both of these. Why is the proof expected to be  
local? And why is filedes\_impl being exposed?

~SheaOn Sat, Aug 30, 2014 at 10:09:11PM -0400, Hongwei Xi wrote:

> The code should be in a DATS file.
> 
> On Sat, Aug 30, 2014 at 10:06 PM, Shea Levy [sh...@shealevy.com](mailto:sh...@shealevy.com) wrote:
> 
> > Hm, this fails with
> > 
> > > error(parsing): the syntactic entity [colonwith] is needed.
> > 
> > ~Shea
> > 
> > On Sat, Aug 30, 2014 at 06:16:13PM -0700, gmhwxi wrote:
> > 
> > > If I understand your situation correctly, I would do something like this:
> > > 
> > > prval  
> > > stderr\_fileno\_pf = \_\_assert () where  
> > > {  
> > > extern praxi \_\_assert (): filedes(2)  
> > > }
> > > 
> > > On Saturday, August 30, 2014 7:31:53 PM UTC-4, Shea Levy wrote:
> > > 
> > > > Hi all,
> > > > 
> > > > I have an abstract view ‘filedes’ parameterized by an int file  
> > > > descriptor. I want to declare that, at the beginning of the program,  
> > > > stderr is an open file, so I have this line in fd.sats:
> > > > 
> > > > > prval stderr\_fileno\_pf : filedes(2)
> > > > 
> > > > Typechecking fails with
> > > > 
> > > > > the static expression is of the sort [S2RTbas(S2RTBASimp(7; view))]  
> > > > > but  
> > > > > it is expectecd to be of the sort [S2RTbas(S2RTBASimp(5; prop))]
> > > > 
> > > > which is clear enough, but if prval is not the right way to go how do I  
> > > > declare a view proof value?
> > > > 
> > > > ~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](mailto:ats-lang-user...@googlegroups.com).  
> > > To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> > > Visit this group at [http://groups.google.com/group/ats-lang-users](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/e05c4c07-2cc3-4586-8d12-22f818f5043f%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/e05c4c07-2cc3-4586-8d12-22f818f5043f%40googlegroups.com)  
> > > .
> > 
> > –  
> > 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](mailto:ats-lang-user...@googlegroups.com).  
> > To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> > Visit this group at [http://groups.google.com/group/ats-lang-users](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/20140831020626.GD7772%40nixos.hsd1.nh.comcast.net](https://groups.google.com/d/msgid/ats-lang-users/20140831020626.GD7772%40nixos.hsd1.nh.comcast.net)  
> > .
> 
> –  
> 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](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](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/CAPPSPLr4npLL9EzmQE3eEL4%3DG1EaPn%3DKfUDkdx86ukXVp%3DC8RA%40mail.gmail.com](https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLr4npLL9EzmQE3eEL4%3DG1EaPn%3DKfUDkdx86ukXVp%3DC8RA%40mail.gmail.com).

---

<div class="post-metadata">

**Author:** ![Shea\_Levy](https://avatars.discourse-cdn.com/v4/letter/s/b38774/32.png) [@Shea\_Levy](https://discourse.ats-lang.org/u/Shea_Levy)\
**Post date:** [August 31, 2014, 3:01am UTC](https://discourse.ats-lang.org/t/declaring-an-external-view-prval/271/6 "2014-08-31T03:01:26Z")

</div>

Ah, I see, so is there no way to modularly declare a linear proof like  
this? I have to have a praxi in every function that uses it?On Sat, Aug 30, 2014 at 07:56:25PM -0700, gmhwxi wrote:

> First,
> 
> %{# should be changed to %{^
> 
> %{# should only be used in a SATS file.
> 
> You code should look like this:
> 
> %{^ #include “include/common.h” %}  
> staload “static/fd.sats” //  
> // staload “dynamic/fd.dats” //  
> implement main () = let  
> prval pf = make () where  
> {  
> extern make (): filedes(2)  
> }  
> val \_ = close(stderr\_fileno\_pf | 2) in 0 end
> 
> On Saturday, August 30, 2014 10:44:03 PM UTC-4, Shea Levy wrote:
> 
> > Ah, I see. I’m now stuck at an error I don’t understand. My code is at  
> > [1](https://github.com/shlevy/socket-activate/blob/WIP/dynamic/socket-activate.dats), [2](https://github.com/shlevy/socket-activate/blob/WIP/static/fd.sats), and [3](https://github.com/shlevy/socket-activate/blob/WIP/dynamic/fd.dats), and the errors I get are:
> > 
> > > /home/shlevy/src/socket-activate/dynamic/socket-activate.dats:  
> > > 129(line=9, offs=17) – 145(line=9, offs=33): error(3): the linear dynamic  
> > > variable [stderr\_fileno\_pf$63(-1)] is expected to be local but it is not.  
> > > /home/shlevy/src/socket-activate/dynamic/socket-activate.dats:  
> > > 129(line=9, offs=17) – 145(line=9, offs=33): error(3):  
> > > [/home/hwxi/research/Postiats/git/src/pats\_trans3\_util.dats]: d3exp\_trdn:  
> > > the dynamic expression cannot be assigned the type [S2Eapp(S2Ecst(filedes); S2EVar(1))].  
> > > /home/shlevy/src/socket-activate/dynamic/socket-activate.dats:  
> > > 129(line=9, offs=17) – 145(line=9, offs=33): error(3): mismatch of static  
> > > terms (tyleq):  
> > > The actual term is: S2Eapp(S2Ecst(filedes\_impl); S2Eintinf(2))  
> > > The needed term is: S2Eapp(S2Ecst(filedes); S2EVar(1))
> > 
> > I’m afraid I’m lost for both of these. Why is the proof expected to be  
> > local? And why is filedes\_impl being exposed?
> > 
> > ~Shea
> > 
> > On Sat, Aug 30, 2014 at 10:09:11PM -0400, Hongwei Xi wrote:
> > 
> > > The code should be in a DATS file.
> > > 
> > > On Sat, Aug 30, 2014 at 10:06 PM, Shea Levy \<[sh...@shealevy.com](mailto:sh...@shealevy.com) \<javascript:\>\> wrote:
> > > 
> > > > Hm, this fails with
> > > > 
> > > > > error(parsing): the syntactic entity [colonwith] is needed.
> > > > 
> > > > ~Shea
> > > > 
> > > > On Sat, Aug 30, 2014 at 06:16:13PM -0700, gmhwxi wrote:
> > > > 
> > > > > If I understand your situation correctly, I would do something like  
> > > > > this:
> > > > > 
> > > > > prval  
> > > > > stderr\_fileno\_pf = \_\_assert () where  
> > > > > {  
> > > > > extern praxi \_\_assert (): filedes(2)  
> > > > > }
> > > > > 
> > > > > On Saturday, August 30, 2014 7:31:53 PM UTC-4, Shea Levy wrote:
> > > > > 
> > > > > > Hi all,
> > > > > > 
> > > > > > I have an abstract view ‘filedes’ parameterized by an int file  
> > > > > > descriptor. I want to declare that, at the beginning of the  
> > > > > > program,  
> > > > > > stderr is an open file, so I have this line in fd.sats:
> > > > > > 
> > > > > > > prval stderr\_fileno\_pf : filedes(2)
> > > > > > 
> > > > > > Typechecking fails with
> > > > > > 
> > > > > > > the static expression is of the sort [S2RTbas(S2RTBASimp(7; view))]  
> > > > > > > but  
> > > > > > > it is expectecd to be of the sort [S2RTbas(S2RTBASimp(5; prop))]
> > > > > > 
> > > > > > which is clear enough, but if prval is not the right way to go how  
> > > > > > do I  
> > > > > > declare a view proof value?
> > > > > > 
> > > > > > ~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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > > > > \<javascript:\>.  
> > > > > Visit this group at [http://groups.google.com/group/ats-lang-users](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/e05c4c07-2cc3-4586-8d12-22f818f5043f%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/e05c4c07-2cc3-4586-8d12-22f818f5043f%40googlegroups.com)
> > 
> > > > .
> > > > 
> > > > –  
> > > > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > > > \<javascript:\>.  
> > > > Visit this group at [http://groups.google.com/group/ats-lang-users](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/20140831020626.GD7772%40nixos.hsd1.nh.comcast.net](https://groups.google.com/d/msgid/ats-lang-users/20140831020626.GD7772%40nixos.hsd1.nh.comcast.net)
> > 
> > > > .
> > > 
> > > –  
> > > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > > \<javascript:\>.  
> > > Visit this group at [http://groups.google.com/group/ats-lang-users](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/CAPPSPLr4npLL9EzmQE3eEL4%3DG1EaPn%3DKfUDkdx86ukXVp%3DC8RA%40mail.gmail.com](https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLr4npLL9EzmQE3eEL4%3DG1EaPn%3DKfUDkdx86ukXVp%3DC8RA%40mail.gmail.com).
> 
> –  
> 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](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](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/fb4aefb5-a045-4bf7-8163-9a950ed8b6bd%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/fb4aefb5-a045-4bf7-8163-9a950ed8b6bd%40googlegroups.com).

---

<div class="post-metadata">

**Author:** ![Shea\_Levy](https://avatars.discourse-cdn.com/v4/letter/s/b38774/32.png) [@Shea\_Levy](https://discourse.ats-lang.org/u/Shea_Levy)\
**Post date:** [August 31, 2014, 4:30am UTC](https://discourse.ats-lang.org/t/declaring-an-external-view-prval/271/7 "2014-08-31T04:30:13Z")

</div>

OK, thanks! I’ve now got something working.On Sat, Aug 30, 2014 at 08:09:39PM -0700, gmhwxi wrote:

> A linear proof cannot be shared; it can only be borrowed.  
> This is a complicated issue. For now, the shortcut I showed is  
> probably the easiest way to take.
> 
> On Saturday, August 30, 2014 11:01:29 PM UTC-4, Shea Levy wrote:
> 
> > Ah, I see, so is there no way to modularly declare a linear proof like  
> > this? I have to have a praxi in every function that uses it?
> > 
> > On Sat, Aug 30, 2014 at 07:56:25PM -0700, gmhwxi wrote:
> > 
> > > First,
> > > 
> > > %{# should be changed to %{^
> > > 
> > > %{# should only be used in a SATS file.
> > > 
> > > You code should look like this:
> > > 
> > > %{^ #include “include/common.h” %}  
> > > staload “static/fd.sats” //  
> > > // staload “dynamic/fd.dats” //  
> > > implement main () = let  
> > > prval pf = make () where  
> > > {  
> > > extern make (): filedes(2)  
> > > }  
> > > val \_ = close(stderr\_fileno\_pf | 2) in 0 end
> > > 
> > > On Saturday, August 30, 2014 10:44:03 PM UTC-4, Shea Levy wrote:
> > > 
> > > > Ah, I see. I’m now stuck at an error I don’t understand. My code is at  
> > > > [1], [2](https://github.com/shlevy/socket-activate/blob/WIP/static/fd.sats), and [3](https://github.com/shlevy/socket-activate/blob/WIP/dynamic/fd.dats), and the errors I get are:
> > > > 
> > > > > /home/shlevy/src/socket-activate/dynamic/socket-activate.dats:  
> > > > > 129(line=9, offs=17) – 145(line=9, offs=33): error(3): the linear  
> > > > > dynamic  
> > > > > variable [stderr\_fileno\_pf$63(-1)] is expected to be local but it is  
> > > > > not.  
> > > > > /home/shlevy/src/socket-activate/dynamic/socket-activate.dats:  
> > > > > 129(line=9, offs=17) – 145(line=9, offs=33): error(3):  
> > > > > [/home/hwxi/research/Postiats/git/src/pats\_trans3\_util.dats]:  
> > > > > d3exp\_trdn:  
> > > > > the dynamic expression cannot be assigned the type  
> > > > > [S2Eapp(S2Ecst(filedes); S2EVar(1))].  
> > > > > /home/shlevy/src/socket-activate/dynamic/socket-activate.dats:  
> > > > > 129(line=9, offs=17) – 145(line=9, offs=33): error(3): mismatch of  
> > > > > static  
> > > > > terms (tyleq):  
> > > > > The actual term is: S2Eapp(S2Ecst(filedes\_impl); S2Eintinf(2))  
> > > > > The needed term is: S2Eapp(S2Ecst(filedes); S2EVar(1))
> > > > 
> > > > I’m afraid I’m lost for both of these. Why is the proof expected to be  
> > > > local? And why is filedes\_impl being exposed?
> > > > 
> > > > [1]:
> > 
> > [https://github.com/shlevy/socket-activate/blob/WIP/dynamic/socket-activate.dats](https://github.com/shlevy/socket-activate/blob/WIP/dynamic/socket-activate.dats)
> > 
> > > > ~Shea
> > > > 
> > > > On Sat, Aug 30, 2014 at 10:09:11PM -0400, Hongwei Xi wrote:
> > > > 
> > > > > The code should be in a DATS file.
> > > > > 
> > > > > On Sat, Aug 30, 2014 at 10:06 PM, Shea Levy \<[sh...@shealevy.com](mailto:sh...@shealevy.com) \<javascript:\>\> wrote:
> > > > > 
> > > > > > Hm, this fails with
> > > > > > 
> > > > > > > error(parsing): the syntactic entity [colonwith] is needed.
> > > > > > 
> > > > > > ~Shea
> > > > > > 
> > > > > > On Sat, Aug 30, 2014 at 06:16:13PM -0700, gmhwxi wrote:
> > > > > > 
> > > > > > > If I understand your situation correctly, I would do something  
> > > > > > > like  
> > > > > > > this:
> > > > > > > 
> > > > > > > prval  
> > > > > > > stderr\_fileno\_pf = \_\_assert () where  
> > > > > > > {  
> > > > > > > extern praxi \_\_assert (): filedes(2)  
> > > > > > > }
> > > > > > > 
> > > > > > > On Saturday, August 30, 2014 7:31:53 PM UTC-4, Shea Levy wrote:
> > > > > > > 
> > > > > > > > Hi all,
> > > > > > > > 
> > > > > > > > I have an abstract view ‘filedes’ parameterized by an int file  
> > > > > > > > descriptor. I want to declare that, at the beginning of the  
> > > > > > > > program,  
> > > > > > > > stderr is an open file, so I have this line in fd.sats:
> > > > > > > > 
> > > > > > > > > prval stderr\_fileno\_pf : filedes(2)
> > > > > > > > 
> > > > > > > > Typechecking fails with
> > > > > > > > 
> > > > > > > > > the static expression is of the sort [S2RTbas(S2RTBASimp(7; view))]  
> > > > > > > > > but  
> > > > > > > > > it is expectecd to be of the sort [S2RTbas(S2RTBASimp(5; prop))]
> > > > > > > > 
> > > > > > > > which is clear enough, but if prval is not the right way to go  
> > > > > > > > how  
> > > > > > > > do I  
> > > > > > > > declare a view proof value?
> > > > > > > > 
> > > > > > > > ~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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > > > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > > > > > > \<javascript:\>.  
> > > > > > > Visit this group at  
> > > > > > > [http://groups.google.com/group/ats-lang-users](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/e05c4c07-2cc3-4586-8d12-22f818f5043f%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/e05c4c07-2cc3-4586-8d12-22f818f5043f%40googlegroups.com)
> > 
> > > > > > .
> > > > > > 
> > > > > > –  
> > > > > > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > > > > > \<javascript:\>.  
> > > > > > Visit this group at [http://groups.google.com/group/ats-lang-users](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/20140831020626.GD7772%40nixos.hsd1.nh.comcast.net](https://groups.google.com/d/msgid/ats-lang-users/20140831020626.GD7772%40nixos.hsd1.nh.comcast.net)
> > 
> > > > > > .
> > > > > 
> > > > > –  
> > > > > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > > > > \<javascript:\>.  
> > > > > Visit this group at [http://groups.google.com/group/ats-lang-users](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/CAPPSPLr4npLL9EzmQE3eEL4%3DG1EaPn%3DKfUDkdx86ukXVp%3DC8RA%40mail.gmail.com](https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLr4npLL9EzmQE3eEL4%3DG1EaPn%3DKfUDkdx86ukXVp%3DC8RA%40mail.gmail.com).
> > 
> > > > 
> > > 
> > > –  
> > > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > > \<javascript:\>.  
> > > Visit this group at [http://groups.google.com/group/ats-lang-users](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/fb4aefb5-a045-4bf7-8163-9a950ed8b6bd%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/fb4aefb5-a045-4bf7-8163-9a950ed8b6bd%40googlegroups.com).
> 
> –  
> 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](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](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/53567894-42a1-4851-a29f-f6643ebff311%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/53567894-42a1-4851-a29f-f6643ebff311%40googlegroups.com).

---

<div class="post-metadata">

**Author:** ![Shea\_Levy](https://avatars.discourse-cdn.com/v4/letter/s/b38774/32.png) [@Shea\_Levy](https://discourse.ats-lang.org/u/Shea_Levy)\
**Post date:** [August 31, 2014, 2:06am UTC](https://discourse.ats-lang.org/t/declaring-an-external-view-prval/271/8 "2014-08-31T02:06:26Z")

</div>

Hm, this fails with

> error(parsing): the syntactic entity [colonwith] is needed.

~SheaOn Sat, Aug 30, 2014 at 06:16:13PM -0700, gmhwxi wrote:

> If I understand your situation correctly, I would do something like this:
> 
> prval  
> stderr\_fileno\_pf = \_\_assert () where  
> {  
> extern praxi \_\_assert (): filedes(2)  
> }
> 
> On Saturday, August 30, 2014 7:31:53 PM UTC-4, Shea Levy wrote:
> 
> > Hi all,
> > 
> > I have an abstract view ‘filedes’ parameterized by an int file  
> > descriptor. I want to declare that, at the beginning of the program,  
> > stderr is an open file, so I have this line in fd.sats:
> > 
> > > prval stderr\_fileno\_pf : filedes(2)
> > 
> > Typechecking fails with
> > 
> > > the static expression is of the sort [S2RTbas(S2RTBASimp(7; view))] but  
> > > it is expectecd to be of the sort [S2RTbas(S2RTBASimp(5; prop))]
> > 
> > which is clear enough, but if prval is not the right way to go how do I  
> > declare a view proof value?
> > 
> > ~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](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](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/e05c4c07-2cc3-4586-8d12-22f818f5043f%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/e05c4c07-2cc3-4586-8d12-22f818f5043f%40googlegroups.com).

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [August 31, 2014, 1:16am UTC](https://discourse.ats-lang.org/t/declaring-an-external-view-prval/271/9 "2014-08-31T01:16:13Z")

</div>

If I understand your situation correctly, I would do something like this:

prval  
stderr\_fileno\_pf = \_\_assert () where  
{  
extern praxi \_\_assert (): filedes(2)  
}On Saturday, August 30, 2014 7:31:53 PM UTC-4, Shea Levy wrote:

> Hi all,
> 
> I have an abstract view ‘filedes’ parameterized by an int file  
> descriptor. I want to declare that, at the beginning of the program,  
> stderr is an open file, so I have this line in fd.sats:
> 
> > prval stderr\_fileno\_pf : filedes(2)
> 
> Typechecking fails with
> 
> > the static expression is of the sort [S2RTbas(S2RTBASimp(7; view))] but  
> > it is expectecd to be of the sort [S2RTbas(S2RTBASimp(5; prop))]
> 
> which is clear enough, but if prval is not the right way to go how do I  
> declare a view proof value?
> 
> ~Shea