diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-23 14:33:18 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-23 14:33:18 +0100 |
| commit | 52b9e2f139444f012f3610e60321e4336d888bec (patch) | |
| tree | f7aac0de77f020d7afb5f3a54fe1acf5bfd63ab6 /src/Core/Generic.idr | |
| parent | 68d030ad604684c257538f0e2d3722d5de435d28 (diff) | |
Prove escape theorems.
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 |