Hacker News new | past | comments | ask | show | jobs | submit login

You say you have dependent types

OK, could you define this?

    data Eq : {a : Type} -> a -> a -> Type where
        Refl : Eq x x

    sym : {x : a} -> {y : a} -> Eq x y -> Eq y x
    sym Refl = Refl

    replace : {a : Type} -> {x : a} -> {y : a} -> {f : a -> Type} -> Eq x y -> f x -> f y
    replace Refl p = p



Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: