<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">2016-04-17 1:00 GMT+02:00 David Christiansen <span dir="ltr"><<a href="mailto:david@davidchristiansen.dk" target="_blank">david@davidchristiansen.dk</a>></span>:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><span class=""><br>
> Kial la tipa kontrolilo ne uzas mian antaŭan pruvon 'incX≡' por unuaigi<br>
> la tipon ⟨ incΩ (y + x) (suc″ (x , y)) ⟩ kun ⟨ suc x , y ⟩ ?<br>
<br>
</span>La unuaigilo ne povas uzi pruvojn, ĉar ĝi devus provi ĉiujn pruvojn en<br>
la tuta sistemo antaŭ ĝi povus malakcepti programon. Se oni volus havi<br>
sistemon en kio la tipkontrolproblemo decideblas, oni devus rekte uzi<br>
pruvobjektojn.<br>
<span class=""><br>
> Ĉu ekzistas metodo por fari tion?<br>
<br>
</span>Novaj versioj de Agda havas REWRITE-regulojn, sed ĝi estas iomete<br>
danĝera. Provu anstataŭe uzi rewrite-sintakson je la maldekstra sido,<br>
laŭ:<br>
<a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.PatternMatching" rel="noreferrer" target="_blank">http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.PatternMatching</a></blockquote><div><br></div><div>Yes that's a good idea, but please look here instead:</div><div><br></div><div><a href="http://agda.readthedocs.org/en/latest/language/with-abstraction.html">http://agda.readthedocs.org/en/latest/language/with-abstraction.html</a><br></div><div><br></div><div>The ReferenceManual section on the wiki has been abandoned in favour of <a href="http://readthedocs.org">readthedocs.org</a>.</div><div><br></div><div>/ Ulf</div></div></div></div>