Hlavní navigace

Názor ke článku Jemný úvod do jazyka Idris (2) - Některé výrazy jsou si rovnější od v - zkusil jsem proof2 přepsat do trochu jiné formy,...

  • 10. 12. 2018 19:07

    v (neregistrovaný) 85.135.6.---

    zkusil jsem proof2 přepsat do trochu jiné formy, která by mohla něco osvětlit:

    --jen synonymum
    Equals : a -> b -> Type
    Equals a b = a = b

    total
    proof2' : (planet:Planet) -> Equals planet Mercury -> Equals (on_mercury planet) True
    proof2' Mercury Refl = Refl
    proof2' Venus Refl impossible
    proof2' Earth Refl impossible
    proof2' Mars Refl impossible
    proof2' Jupiter Refl impossible
    proof2' Saturn Refl impossible
    proof2' Uranus Refl impossible
    proof2' Neptune Refl impossible