Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
reflexivity in Idris
infixl 5
data (⇔) : a -> b -> Type where
Refl_ : x ⇔ x -- there is an identity, a function/path/morphism from a value of x of Type a to itself. /or to a value of an isomorphic type!/
fiveIsFive : 5 ⇔ 5
-- this is a function of type "equality" parametrized by "5" and "5" and since it has a constructor and is thus populated (by Refl), the Type with this parameters is populated and it is a proof that five does, indeed, equal itself.
fiveIsFive = Refl_
twoPlusTwo : 2 + 2 ⇔ 4
twoPlusTwo = Refl_
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.