Hlavní navigace

Názor ke článku Jemný úvod do jazyka Idris (2) - Některé výrazy jsou si rovnější od BoneFlute - Mohl by si mi prosím trochu rozvést to...

  • 8. 12. 2018 13:32

    BoneFlute

    Mohl by si mi prosím trochu rozvést to s tím `Refl` ?

    Druhý a třetí snippet v pohodě. Ale k čemu slouží ten čtvrtý? To, že po Merkuru je Venuše je definováno v třetím snippetu. Takže co v tom čtvrtém činím? Čeho tím dosáhnu? Jak se ten důkaz použije/uplatní?

    Čtvrtý snippet jasný. Ale u toho pátého mi nedochází ta syntaxe.

    Možná taky dojíždím na tom, že nerozumím tomu vzorci "(∀p:Planet)p=Mer­cury⊃onMercury(p)" - pro všechny planety platí, že pokud p je Merkur, tak pokud jsem na planetě tak to musí být Merkur ? :-( Uff.

    Ospravedlňujem se, nejsem v této úrovni matematiky tak dobrý. Jsem Haskellista samouk.