Add %default total to a few modules

libs/base/Data/Either.idr

@@ -1,5 +1,7 @@
 module Data.Either
 
+%default total
+
 ||| True if the argument is Left, False otherwise
 public export
 isLeft : Either a b -> Bool
@@ -68,7 +70,6 @@ eitherToMaybe (Right x) = Just x
 -- Injectivity of constructors
 
 ||| Left is injective
-total
 leftInjective : {b : Type}
              -> {x : a}
              -> {y : a}
@@ -76,7 +77,6 @@ leftInjective : {b : Type}
 leftInjective Refl = Refl
 
 ||| Right is injective
-total
 rightInjective : {a : Type}
               -> {x : b}
               -> {y : b}

libs/base/Data/Fin.idr

@@ -4,6 +4,8 @@ import public Data.Maybe
 import Data.Nat
 import Decidable.Equality
 
+%default total
+
 ||| Numbers strictly less than some bound.  The name comes from "finite sets".
 |||
 ||| It's probably not a good idea to use `Fin` for arithmetic, and they will be
@@ -111,7 +113,7 @@ last : {n : _} -> Fin (S n)
 last {n=Z} = FZ
 last {n=S _} = FS last
 
-public export total
+public export
 FSinjective : {f : Fin n} -> {f' : Fin n} -> (FS f = FS f') -> f = f'
 FSinjective Refl = Refl
 
@@ -165,7 +167,7 @@ restrict n val = let val' = assert_total (abs (mod val (cast (S n)))) in
 -- DecEq
 --------------------------------------------------------------------------------
 
-export total
+export
 FZNotFS : {f : Fin n} -> FZ {k = n} = FS f -> Void
 FZNotFS Refl impossible
 
@@ -178,4 +180,3 @@ implementation DecEq (Fin n) where
       = case decEq f f' of
              Yes p => Yes $ cong FS p
              No p => No $ \h => p $ FSinjective {f = f} {f' = f'} h
-

libs/base/Data/List/Views.idr

@@ -5,6 +5,8 @@ import Data.List
 import Data.Nat
 import Data.Nat.Views
 
+%default total
+
 lengthSuc : (xs : List a) -> (y : a) -> (ys : List a) ->
             length (xs ++ (y :: ys)) = S (length (xs ++ ys))
 lengthSuc [] _ _ = Refl
@@ -62,7 +64,7 @@ data SplitRec : List a -> Type where
 
 ||| Covering function for the `SplitRec` view
 ||| Constructs the view in O(n lg n)
-public export total
+public export
 splitRec : (xs : List a) -> SplitRec xs
 splitRec xs with (sizeAccessible xs)
   splitRec xs | acc with (split xs)
@@ -92,5 +94,3 @@ snocListHelp snoc (x :: xs)
 export
 snocList : (xs : List a) -> SnocList xs
 snocList xs = snocListHelp Empty xs
-
-

libs/base/Data/Nat.idr

@@ -241,7 +241,7 @@ data CmpNat : Nat -> Nat -> Type where
      CmpGT : (x : _) -> CmpNat (y + S x) y
 
 export
-total cmp : (x, y : Nat) -> CmpNat x y
+cmp : (x, y : Nat) -> CmpNat x y
 cmp Z Z     = CmpEQ
 cmp Z (S k) = CmpLT _
 cmp (S k) Z = CmpGT _

libs/base/Data/Nat/Views.idr

@@ -3,6 +3,8 @@ module Data.Nat.Views
 import Control.WellFounded
 import Data.Nat
 
+%default total
+
 ||| View for dividing a Nat in half
 public export
 data Half : Nat -> Type where
@@ -25,7 +27,7 @@ half (S k) with (half k)
                                            HalfEven (S n)
   half (S (n + n)) | HalfEven n = HalfOdd n
 
-public export total
+public export
 halfRec : (n : Nat) -> HalfRec n
 halfRec n with (sizeAccessible n)
   halfRec  Z | acc = HalfRecZ

libs/base/Decidable/Equality.idr

@@ -3,6 +3,8 @@ module Decidable.Equality
 import Data.Maybe
 import Data.Nat
 
+%default total
+
 --------------------------------------------------------------------------------
 -- Decidable equality
 --------------------------------------------------------------------------------
@@ -11,19 +13,19 @@ import Data.Nat
 public export
 interface DecEq t where
   ||| Decide whether two elements of `t` are propositionally equal
-  total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
+  decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
 
 --------------------------------------------------------------------------------
 -- Utility lemmas
 --------------------------------------------------------------------------------
 
 ||| The negation of equality is symmetric (follows from symmetry of equality)
-export total
+export
 negEqSym : forall a, b . (a = b -> Void) -> (b = a -> Void)
 negEqSym p h = p (sym h)
 
 ||| Everything is decidably equal to itself
-export total
+export
 decEqSelfIsYes : DecEq a => {x : a} -> decEq x x = Yes Refl
 decEqSelfIsYes {x} with (decEq x x)
   decEqSelfIsYes {x} | Yes Refl = Refl
@@ -40,7 +42,7 @@ implementation DecEq () where
 --------------------------------------------------------------------------------
 -- Booleans
 --------------------------------------------------------------------------------
-total trueNotFalse : True = False -> Void
+trueNotFalse : True = False -> Void
 trueNotFalse Refl impossible
 
 export
@@ -54,7 +56,7 @@ implementation DecEq Bool where
 -- Nat
 --------------------------------------------------------------------------------
 
-total ZnotS : Z = S n -> Void
+ZnotS : Z = S n -> Void
 ZnotS Refl impossible
 
 export
@@ -70,7 +72,7 @@ implementation DecEq Nat where
 -- Maybe
 --------------------------------------------------------------------------------
 
-total nothingNotJust : {x : t} -> (Nothing {ty = t} = Just x) -> Void
+nothingNotJust : {x : t} -> (Nothing {ty = t} = Just x) -> Void
 nothingNotJust Refl impossible
 
 export
@@ -196,4 +198,3 @@ implementation DecEq String where
              primitiveEq = believe_me (Refl {x})
              primitiveNotEq : forall x, y . x = y -> Void
              primitiveNotEq prf = believe_me {b = Void} ()
-