# How to return proof function using vtakeout?

**URL:** <https://discourse.ats-lang.org/t/how-to-return-proof-function-using-vtakeout/70>\
**Category:** Google Group\
**Created:** [January 12, 2014, 1:38pm UTC](https://discourse.ats-lang.org/t/how-to-return-proof-function-using-vtakeout/70 "2014-01-12T13:38:50Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![Chotu\_S](https://avatars.discourse-cdn.com/v4/letter/c/7cd45c/32.png) [@Chotu\_S](https://discourse.ats-lang.org/u/Chotu_S)\
**Post date:** [January 12, 2014, 1:38pm UTC](https://discourse.ats-lang.org/t/how-to-return-proof-function-using-vtakeout/70/1 "2014-01-12T13:38:50Z")

</div>

Suppose I want a function that given a proof of non empty list return a  
tuple consisting of proof of at-view of first node and a proof function  
that takes that at-view and returns the original list.

I am unable to make such function , here is the code for my attempt :

dataview slseg\_v (a:t@ype, int(_len_) , addr(_beg_) , addr(_end_)) =  
| {l:addr} slseg\_v\_nil(a,0,l,l) of ()  
| {n:nat} {l\_fst : agz} {l\_nxt :addr} {l\_end : addr}  
slseg\_v\_cons (a,n+1,l\_fst,l\_end) of  
( (a,ptr l\_nxt) @ l\_fst , slseg\_v(a , n , l\_nxt , l\_end))

viewdef sl\_v  
(a:t@ype , n:int, l:addr) = slseg\_v(a,n,l,null)

extern  
prfun lst2at{a:t@ype} {l:agz} {n:nat | n \> 0}  
(pf1: sl\_v(a,n,l) ) :  
vtakeout (sl\_v (a,n,l) , [m:addr] (a,ptr m) @ l)  
// ((a,ptr m) @ l , (a,ptr m) @ l -\> sl\_v (a,n,l))

primplement  
lst2at (pf1) = let  
prval slseg\_v\_cons (pf\_at , pf\_lst) = pf1  
in  
(pf\_at , llam pf\_at = (pf\_at , pf\_lst))  
end

Thanks

---

<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:** [January 12, 2014, 4:39pm UTC](https://discourse.ats-lang.org/t/how-to-return-proof-function-using-vtakeout/70/2 "2014-01-12T16:39:47Z")

</div>

Following is a version that type-checks. The syntax #[… | …] is for  
forming a value of existential type.

dataview  
slseg\_v  
(  
a:t@ype, int(_len_) , addr(_beg_) , addr(_end_)  
) =  
| {l:addr} slseg\_v\_nil(a,0,l,l) of ()  
| {n:nat} {l\_fst : agz} {l\_nxt :addr} {l\_end : addr}  
slseg\_v\_cons (a,n+1,l\_fst,l\_end) of  
( (a,ptr l\_nxt) @ l\_fst , slseg\_v(a , n , l\_nxt , l\_end))

viewdef sl\_v (a:t@ype , n:int, l:addr) = slseg\_v(a,n,l,null)

extern  
prfun  
lst2at{a:t@ype}{l:agz}{n:int | n \> 0}  
(pf1: sl\_v(a,n,l)) : [m:addr] vtakeout (sl\_v (a,n,l), (a,ptr m) @ l)

primplement  
lst2at (pf1) = let  
prval slseg\_v\_cons (pf\_at , pf\_lst) = pf1  
in  
#[… | (pf\_at , llam pf\_at = slseg\_v\_cons (pf\_at , pf\_lst))]  
end // end of [lst2at]On Sunday, January 12, 2014 8:38:50 AM UTC-5, chota singh wrote:

> Suppose I want a function that given a proof of non empty list return a  
> tuple consisting of proof of at-view of first node and a proof function  
> that takes that at-view and returns the original list.
> 
> I am unable to make such function , here is the code for my attempt :
> 
> dataview slseg\_v (a:t@ype, int(_len_) , addr(_beg_) , addr(_end_)) =  
> | {l:addr} slseg\_v\_nil(a,0,l,l) of ()  
> | {n:nat} {l\_fst : agz} {l\_nxt :addr} {l\_end : addr}  
> slseg\_v\_cons (a,n+1,l\_fst,l\_end) of  
> ( (a,ptr l\_nxt) @ l\_fst , slseg\_v(a , n , l\_nxt , l\_end))
> 
> viewdef sl\_v  
> (a:t@ype , n:int, l:addr) = slseg\_v(a,n,l,null)
> 
> extern  
> prfun lst2at{a:t@ype} {l:agz} {n:nat | n \> 0}  
> (pf1: sl\_v(a,n,l) ) :  
> vtakeout (sl\_v (a,n,l) , [m:addr] (a,ptr m) @ l)  
> // ((a,ptr m) @ l , (a,ptr m) @ l → sl\_v (a,n,l))
> 
> primplement  
> lst2at (pf1) = let  
> prval slseg\_v\_cons (pf\_at , pf\_lst) = pf1  
> in  
> (pf\_at , llam pf\_at = (pf\_at , pf\_lst))  
> end
> 
> Thanks

---

<div class="post-metadata">

**Author:** ![Chotu\_S](https://avatars.discourse-cdn.com/v4/letter/c/7cd45c/32.png) [@Chotu\_S](https://discourse.ats-lang.org/u/Chotu_S)\
**Post date:** [January 13, 2014, 6:18am UTC](https://discourse.ats-lang.org/t/how-to-return-proof-function-using-vtakeout/70/3 "2014-01-13T06:18:04Z")

</div>

Thanks it now compiles . I just realize that I had also forgot to put the  
constructor in my original post 🙂 .On Sunday, January 12, 2014 10:09:47 PM UTC+5:30, gmhwxi wrote:

> Following is a version that type-checks. The syntax #[… | …] is for  
> forming a value of existential type.
> 
> dataview  
> slseg\_v  
> (  
> a:t@ype, int(_len_) , addr(_beg_) , addr(_end_)  
> ) =  
> | {l:addr} slseg\_v\_nil(a,0,l,l) of ()  
> | {n:nat} {l\_fst : agz} {l\_nxt :addr} {l\_end : addr}  
> slseg\_v\_cons (a,n+1,l\_fst,l\_end) of  
> ( (a,ptr l\_nxt) @ l\_fst , slseg\_v(a , n , l\_nxt , l\_end))
> 
> viewdef sl\_v (a:t@ype , n:int, l:addr) = slseg\_v(a,n,l,null)
> 
> extern  
> prfun  
> lst2at{a:t@ype}{l:agz}{n:int | n \> 0}  
> (pf1: sl\_v(a,n,l)) : [m:addr] vtakeout (sl\_v (a,n,l), (a,ptr m) @ l  
> )
> 
> primplement  
> lst2at (pf1) = let  
> prval slseg\_v\_cons (pf\_at , pf\_lst) = pf1  
> in  
> #[… | (pf\_at , llam pf\_at = slseg\_v\_cons (pf\_at , pf\_lst))]  
> end // end of [lst2at]
> 
> On Sunday, January 12, 2014 8:38:50 AM UTC-5, chota singh wrote:
> 
> > Suppose I want a function that given a proof of non empty list return a  
> > tuple consisting of proof of at-view of first node and a proof function  
> > that takes that at-view and returns the original list.
> > 
> > I am unable to make such function , here is the code for my attempt :
> > 
> > dataview slseg\_v (a:t@ype, int(_len_) , addr(_beg_) , addr(_end_)) =  
> > | {l:addr} slseg\_v\_nil(a,0,l,l) of ()  
> > | {n:nat} {l\_fst : agz} {l\_nxt :addr} {l\_end : addr}  
> > slseg\_v\_cons (a,n+1,l\_fst,l\_end) of  
> > ( (a,ptr l\_nxt) @ l\_fst , slseg\_v(a , n , l\_nxt , l\_end))
> > 
> > viewdef sl\_v  
> > (a:t@ype , n:int, l:addr) = slseg\_v(a,n,l,null)
> > 
> > extern  
> > prfun lst2at{a:t@ype} {l:agz} {n:nat | n \> 0}  
> > (pf1: sl\_v(a,n,l) ) :  
> > vtakeout (sl\_v (a,n,l) , [m:addr] (a,ptr m) @ l)  
> > // ((a,ptr m) @ l , (a,ptr m) @ l → sl\_v (a,n,l))
> > 
> > primplement  
> > lst2at (pf1) = let  
> > prval slseg\_v\_cons (pf\_at , pf\_lst) = pf1  
> > in  
> > (pf\_at , llam pf\_at = (pf\_at , pf\_lst))  
> > end
> > 
> > Thanks