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

%inline

Browse source
This commit is contained in:
rhiannon morris 2023-02-19 17:43:14 +01:00
parent 810de09f61
commit 27e61011ac
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
lib/Quox/Equal.idr
View file

@ -188,7 +188,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
||| compares two types, using the current variance `mode` for universes. ||| compares two types, using the current variance `mode` for universes.
||| fails if they are not types, even if they would happen to be equal. ||| fails if they are not types, even if they would happen to be equal.
export covering export covering %inline
compareType : TContext q 0 n -> (s, t : Term q 0 n) -> m () compareType : TContext q 0 n -> (s, t : Term q 0 n) -> m ()
compareType ctx s t = do compareType ctx s t = do
let Element s ns = whnfD defs s let Element s ns = whnfD defs s

4
lib/Quox/Syntax/DimEq.idr
View file

@ -28,11 +28,11 @@ data DimEq : Nat -> Type where
%name DimEq eqs %name DimEq eqs
export export %inline
zeroEq : DimEq 0 zeroEq : DimEq 0
zeroEq = C [<] zeroEq = C [<]
export export %inline
new' : {d : Nat} -> DimEq' d new' : {d : Nat} -> DimEq' d
new' {d = 0} = [<] new' {d = 0} = [<]
new' {d = S d} = new' :< Nothing new' {d = S d} = new' :< Nothing