diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-06-09 16:00:39 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-06-09 16:00:39 +0100 |
| commit | f910e142ce7c10f8244ecfa40e41756fb8c8a53f (patch) | |
| tree | c55fc84064edea55c01d3f93733b878b245aa14f /src/Total/Term.idr | |
| parent | d5794f15b40ef4c683d713ffad027e94f2caf17e (diff) | |
Use co-deBruijn syntax in logical relation proof.master
Many proofs are still missing. Because they are erased, the program
still runs fine without them.
Diffstat (limited to 'src/Total/Term.idr')
| -rw-r--r-- | src/Total/Term.idr | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Total/Term.idr b/src/Total/Term.idr index 8e3e42a..129662a 100644 --- a/src/Total/Term.idr +++ b/src/Total/Term.idr @@ -77,6 +77,7 @@ sub2 . (sub1 :< t) = sub2 . sub1 :< subst t sub2 -- Utilities +export cong3 : (0 f : a -> b -> c -> d) -> x1 = x2 -> y1 = y2 -> z1 = z2 -> f x1 y1 z1 = f x2 y2 z2 cong3 f Refl Refl Refl = Refl |