<div dir="ltr"><div>Hello:</div><div><br></div>Just wanna make sure.<div>In the sorting example, we gave it the type<div><br></div><div>    sort : (xs : [N]) -> \exists ( \ys -> Perm xs ys * Ordered ys )<br></div><div>

<br></div><div>Similarly, in the maximum function, we have the type</div><div><br></div><div>    max : (xs : [N]) -> (xs /= []) -> \exists ( Sup xs )</div><div><br></div><div>and `Sup xs` is also a function.</div><div>
<br></div><div>
Why wouldn't we give the proof directly, but rather uses</div></div><div>assertions that when given a parameter, tries to (re-?)construct</div><div>the proof?</div><div class="gmail_extra"><br>suhorng</div><div class="gmail_extra">
<br><div class="gmail_quote">2013/9/6 Shin-Cheng Mu <span dir="ltr"><<a href="mailto:scm@iis.sinica.edu.tw" target="_blank">scm@iis.sinica.edu.tw</a>></span><br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

Dear friends,<br>
<br>
These are my slides yesterday,<br>
"A Brief Intro. to Dependently Typed Programming"<br>
<br>
<a href="http://pc-scm.iis.sinica.edu.tw/FT20130905.pdf" target="_blank">http://pc-scm.iis.sinica.edu.tw/FT20130905.pdf</a><br>
<br>
sincerely,<br>
Shin<br>
<a href="mailto:scm@iis.sinica.edu.tw" target="_blank">scm@iis.sinica.edu.tw</a><br>
<br>
<br>
<br>
_______________________________________________<br>
Fun-thursday mailing list<br>
<a href="mailto:Fun-thursday@iis.sinica.edu.tw" target="_blank">Fun-thursday@iis.sinica.edu.tw</a><br>
<a href="http://www.iis.sinica.edu.tw/mailman/listinfo/fun-thursday" target="_blank">http://www.iis.sinica.edu.tw/mailman/listinfo/fun-thursday</a><br>
</blockquote></div><br></div></div>