[Agda] Inteligenta tipa kontrolilo?

[Ulf Norell]

2016-04-17 1:00 GMT+02:00 David Christiansen <david at davidchristiansen.dk>:

>
> > Kial la tipa kontrolilo ne uzas mian antaŭan pruvon 'incX≡' por unuaigi
> > la tipon ⟨ incΩ (y + x) (suc″ (x , y)) ⟩ kun ⟨ suc x , y ⟩ ?
>
> La unuaigilo ne povas uzi pruvojn, ĉar ĝi devus provi ĉiujn pruvojn en
> la tuta sistemo antaŭ ĝi povus malakcepti programon. Se oni volus havi
> sistemon en kio la tipkontrolproblemo decideblas, oni devus rekte uzi
> pruvobjektojn.
>
> > Ĉu ekzistas metodo por fari tion?
>
> Novaj versioj de Agda havas REWRITE-regulojn, sed ĝi estas iomete
> danĝera. Provu anstataŭe uzi rewrite-sintakson je la maldekstra sido,
> laŭ:
>
> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.PatternMatching


Yes that's a good idea, but please look here instead:

http://agda.readthedocs.org/en/latest/language/with-abstraction.html

The ReferenceManual section on the wiki has been abandoned in favour of
readthedocs.org.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160417/e4622d50/attachment.html