rhi/quox
rhi
/
quox
1
0
Fork 0
Code Issues 16 Pull Requests 1 Releases Wiki Activity

remove some implicits that can now be inferred

This commit is contained in:
rhiannon morris 2022-02-27 02:06:52 +01:00
parent 3722c769cf
commit 8248f8ed82
3 changed files with 12 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/Quox/Context.idr
View File

@ -102,7 +102,7 @@ Triangle' a = Context $ Context (\_ => a)
export
0 telescopeLTE : Telescope _ from to -> from `LTE` to
telescopeLTE [<] = reflexive {rel=Nat.LTE}
telescopeLTE [<] = reflexive
telescopeLTE (tel :< _) = lteSuccRight $ telescopeLTE tel
export
@ -111,7 +111,7 @@ export
export %hint
0 succGT : S n `GT` n
succGT = LTESucc $ reflexive {rel=Nat.LTE}
succGT = LTESucc reflexive
parameters {auto _ : Applicative f}
@ -176,7 +176,7 @@ namespace Nat
export
lte'ToLte : {n : Nat} -> m `LTE'` n -> m `LTE` n
lte'ToLte LTERefl = reflexive {rel=Nat.LTE}
lte'ToLte LTERefl = reflexive
lte'ToLte (LTESuccR p) = lteSuccRight (lte'ToLte p)
export

8
src/Quox/Syntax/Shift.idr
View File

@ -47,7 +47,7 @@ fromEqv (EqSS e) = cong SS $ fromEqv e
export
0 toEqv : by = bz -> by `Eqv` bz
toEqv Refl {by = SZ} = EqSZ
toEqv Refl {by = (SS by)} = EqSS $ toEqv Refl {by}
toEqv Refl {by = (SS by)} = EqSS $ toEqv Refl
export
@ -60,9 +60,9 @@ export
by.nat + i.nat `LT` to
shiftVarLT by i =
rewrite plusSuccRightSucc by.nat i.nat in
transitive {rel=Nat.LTE}
transitive
(plusLteMonotoneLeft by.nat (S i.nat) from (toNatLT i))
(replace {p=(`LTE` to)} (shiftDiff by) $ reflexive {rel=Nat.LTE})
(replace {p=(`LTE` to)} (shiftDiff by) reflexive)
public export
@ -85,7 +85,7 @@ export
0 toNatInj' : (by : Shift from1 to1) -> (bz : Shift from2 to2) ->
by.nat = bz.nat -> by `Eqv` bz
toNatInj' SZ SZ prf = EqSZ
toNatInj' (SS by) (SS bz) prf = EqSS $ toNatInj' by bz $ succInjective _ _ prf
toNatInj' (SS by) (SS bz) prf = EqSS $ toNatInj' by bz $ injective prf
toNatInj' (SS by) SZ Refl impossible
export

10
src/Quox/Syntax/Var.idr
View File

@ -105,7 +105,7 @@ toFromNat (S k) (LTESucc x) = cong S $ toFromNat k x
-- to be an instance of <https://github.com/idris-lang/Idris2/issues/1259>?
export
weak : (0 p : m `LTE` n) -> Var m -> Var n
weak p i = fromNatWith i.nat $ transitive (toNatLT i) p {rel=LTE}
weak p i = fromNatWith i.nat $ transitive (toNatLT i) p
public export
0 weakSpec : m `LTE` n -> Var m -> Var n
@ -150,7 +150,7 @@ i `GT` j = j `LT` i
export
Transitive (Var n) LT where
transitive LTZ (LTS _) = LTZ
transitive (LTS p) (LTS q) = LTS $ transitive p q {rel = Var.LT}
transitive (LTS p) (LTS q) = LTS $ transitive p q
export Uninhabited (i `Var.LT` i) where uninhabited (LTS p) = uninhabited p
export Uninhabited (VS i `LT` VZ) where uninhabited _ impossible
@ -204,17 +204,17 @@ data LTE : Var n -> Var n -> Type where
export
Reflexive (Var n) LTE where
reflexive {x = VZ} = LTEZ
reflexive {x = VS i} = LTES $ reflexive {x = i}
reflexive {x = VS i} = LTES reflexive
export
Transitive (Var n) LTE where
transitive LTEZ q = LTEZ
transitive (LTES p) (LTES q) = LTES $ transitive p q {rel = Var.LTE}
transitive (LTES p) (LTES q) = LTES $ transitive p q
export
Antisymmetric (Var n) LTE where
antisymmetric LTEZ LTEZ = Refl
antisymmetric (LTES p) (LTES q) = cong VS $ antisymmetric p q {rel = Var.LTE}
antisymmetric (LTES p) (LTES q) = cong VS $ antisymmetric p q
export
splitLTE : {j : Var n} -> i `LTE` j -> Either (i = j) (i `LT` j)