Abt.Class.HEq1

Documentation

class HEq1 f where

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.

Methods

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

Instances

HEq1 [Nat] o => HEq1 Nat (Tm o)

HEq1 [Nat] Lang

HEq1 k el => HEq1 [k] (HList k el)