diff options
Diffstat (limited to 'src/Core/Generic.idr')
| -rw-r--r-- | src/Core/Generic.idr | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Core/Generic.idr b/src/Core/Generic.idr index c2bd1f4..4563063 100644 --- a/src/Core/Generic.idr +++ b/src/Core/Generic.idr @@ -118,6 +118,10 @@ interface IsEq (0 eq : Equality) where --- eq.TypeEq {n} env (Pi a b) (Pi c d) +export +ntrlEqImpliesTypeEq : IsEq eq => eq.NtrlEq {n = k} env n m Set -> eq.TypeEq env n.fst m.fst +ntrlEqImpliesTypeEq = termEqImpliesTypeEq . ntrlEqImpliesTermEq + -- Instance 1 ------------------------------------------------------------------ public export |