[Agda] Inteligenta tipa kontrolilo?

[David Christiansen]

> 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

/David