rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

add missing %default total

Browse source
This commit is contained in:
rhiannon morris 2023-03-27 00:07:39 +02:00
parent 773f6372ea
commit 137962c176
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
lib/Quox/Equal.idr
View file

@ -6,6 +6,8 @@ import public Control.Monad.Either
import public Control.Monad.Reader import public Control.Monad.Reader
import Data.Maybe import Data.Maybe
%default total
public export public export
record CmpContext where record CmpContext where
@ -98,7 +100,7 @@ parameters (defs : Definitions' q g)
||| * all equality types are subsingletons because uip is admissible by ||| * all equality types are subsingletons because uip is admissible by
||| boundary separation. ||| boundary separation.
||| * an enum type is a subsingleton if it has zero or one tags. ||| * an enum type is a subsingleton if it has zero or one tags.
public export public export covering
isSubSing : HasErr q m => {n : Nat} -> Term q 0 n -> m Bool isSubSing : HasErr q m => {n : Nat} -> Term q 0 n -> m Bool
isSubSing ty = do isSubSing ty = do
Element ty nc <- whnfT defs ty Element ty nc <- whnfT defs ty