abt-0.1.1.0: Abstract binding trees for Haskell

Safe HaskellNone
LanguageHaskell2010

Abt.Class.HEq1

Synopsis

Documentation

data a :=: b where Source

Essentially, Martin-Löf's identity type.

Constructors

Refl :: a :=: a 

cong :: (a :=: b) -> f a :=: f b Source

Type constructors are extensional.

class HEq1 f where Source

Uniform variant of Eq for indexed types. This is different from Eq1 in that it is properly kind polymorphic and crucially heterogeneous, and it places no constraint on the index. Because it is heterogeneous, it is useful to project equality in the base space from equality in the total space.

Minimal complete definition

heq1

Methods

heq1 :: f i -> f j -> Maybe (i :=: j) Source

When both sides are equal, give in addition a proof that their indices are equal; otherwise return Nothing.

(===) :: f i -> f j -> Bool Source

A boolean version of heq1, which must agree with it.

Instances

HEq1 [Nat] o => HEq1 Nat (Tm o) 
HEq1 [Nat] Lang 
HEq1 k el => HEq1 [k] (Rec k el)