From 56ddd59fb4e690378656418cd9def4c68e60f48a Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Tue, 12 Apr 2022 16:48:23 +0200
Subject: [PATCH] make lteZero' and lteSucc' into hints

---
 src/Quox/NatExtra.idr | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Quox/NatExtra.idr b/src/Quox/NatExtra.idr
index 0e7bec7..28e2cba 100644
--- a/src/Quox/NatExtra.idr
+++ b/src/Quox/NatExtra.idr
@@ -9,12 +9,12 @@ data LTE' : Nat -> Nat -> Type where
   LTESuccR : LTE' m n -> LTE' m (S n)
 %builtin Natural LTE'
 
-public export
+public export %hint
 lteZero' : {n : Nat} -> LTE' 0 n
 lteZero' {n = 0}   = LTERefl
 lteZero' {n = S n} = LTESuccR lteZero'
 
-public export
+public export %hint
 lteSucc' : LTE' m n -> LTE' (S m) (S n)
 lteSucc' LTERefl      = LTERefl
 lteSucc' (LTESuccR p) = LTESuccR $ lteSucc' p