[Haskell-ELTE] Agda

[Dr. ERDI Gergo]

Sziasztok!

Elkezdtem nezegetni az Agdat, csinalgattam par feladatot, aztan nekilattam 
a klasszikus Peano-aritmetikai tetelek bizonyitasanak. Nagyon ra lehet 
csuszni a cuccra, mihelyst a legelso falakat attorod, mar papirra sincs 
mindig szukseg, hanem lehet rogton beirni a bizonyitasokat:)

Egyelore ott  tartok, hogy a termeszetes szamok felett az alabbi 
muvelet-tulajdonsagokat bizonyitottam be:
 	osszeadas kommutativitasa, asszociativitasa
 	szorzas komm, asszoc, disztributivitas osszeadads felett
 	rendezes reflexiv, tranzitiv, antiszimmetrikus

A forrasfile-okat naprakeszen tartom a git://gergo.erdi.hu/agda repoban; 
varom a kommenteket. Egeszen bizonyos, hogy sokmindent sokkal 
nyakatekertebben oldottam meg, mint lehetett volna (legdurvabb a szorzas 
kommutativitasanak bizonyitasa lett), de az Ulf Norell-f. tutorialnak is 
meg csak kb a felenel tartok.

Udv,
 	Cactus

u.i.: Ha valakinek szuksege van Ubuntu/amd64-hez Agda csomagra, akkor 
tudok segiteni (en csak i386-osat talaltam, es volt egy kis szopas a 
forditassal).

-- 

   .--= ULLA! =-----------------.   `We are not here to give users what
    \     http://gergo.erdi.hu   \   they want'  -- RMS, at GUADEC 2001
     `---= gergo at erdi.hu =-------'
Remember: guns don't kill -- postal workers do.