Skip to content

Commit e91c4e1

Browse files
committed
Fix compilation errors
1 parent 55360ef commit e91c4e1

File tree

2 files changed

+0
-60
lines changed

2 files changed

+0
-60
lines changed

docs/agda-spec/src/Interface/HasOrder/Instance.agda

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -26,10 +26,6 @@ instance
2626

2727
open import Data.Rational using (ℚ)
2828
import Data.Rational.Properties as Rat hiding (_≟_)
29-
30-
ℚ-Dec-≤ = ⁇² Rat._≤?_
31-
ℚ-Dec-< = ⁇² Rat._<?_
32-
3329
ℚ-hasPreorder = hasPreorderFromNonStrict Rat.≤-isPreorder _≟_
3430
ℚ-hasPartialOrder = HasPartialOrder ∋ record { ≤-antisym = Rat.≤-antisym }
3531
ℚ-hasDecPartialOrder = HasDecPartialOrder {A = ℚ} ∋ record {}

docs/agda-spec/src/Tactic/ByEq.agda

Lines changed: 0 additions & 56 deletions
This file was deleted.

0 commit comments

Comments
 (0)