From 5e704f08d1f70e12e4da1f0ed359dd2495852e5f Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Sat, 9 Mar 2024 20:59:16 -0600 Subject: Factor out comparison --- FinMerge.agda | 26 +++++++++--------- FinMerge/Properties.agda | 71 +++++++++++++++++------------------------------- 2 files changed, 38 insertions(+), 59 deletions(-) diff --git a/FinMerge.agda b/FinMerge.agda index 51e7a67..c62fe14 100644 --- a/FinMerge.agda +++ b/FinMerge.agda @@ -1,3 +1,4 @@ +{-# OPTIONS --without-K --safe #-} module FinMerge where open import Data.Empty using (⊥-elim) @@ -6,7 +7,7 @@ open import Data.Fin.Properties using (¬Fin0) open import Data.Nat using (ℕ; _+_; _≤_; _<_ ; z