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

remove some public exports that probably aren't needed

Browse source
This commit is contained in:
rhiannon morris 2021-09-03 17:10:20 +02:00
parent 06e5c09896
commit d41ab0897c
4 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Quox/Pretty.idr
View file

@ -137,11 +137,11 @@ public export
interface PrettyHL a where interface PrettyHL a where
prettyM : HasEnv m => a -> m (Doc HL) prettyM : HasEnv m => a -> m (Doc HL)
public export %inline export %inline
pretty0M : (PrettyHL a, HasEnv m) => a -> m (Doc HL) pretty0M : (PrettyHL a, HasEnv m) => a -> m (Doc HL)
pretty0M = local {prec := Outer} . prettyM pretty0M = local {prec := Outer} . prettyM
public export %inline export %inline
pretty0 : PrettyHL a => {default True unicode : Bool} -> a -> Doc HL pretty0 : PrettyHL a => {default True unicode : Bool} -> a -> Doc HL
pretty0 x {unicode} = pretty0 x {unicode} =
let env = MakePrettyEnv {dnames = [], tnames = [], unicode, prec = Outer} in let env = MakePrettyEnv {dnames = [], tnames = [], unicode, prec = Outer} in

2
src/Quox/Syntax/Shift.idr
View file

@ -49,7 +49,7 @@ toEqv Refl {by = SZ} = EqSZ
toEqv Refl {by = (SS by)} = EqSS $ toEqv Refl {by} toEqv Refl {by = (SS by)} = EqSS $ toEqv Refl {by}
public export export
0 shiftDiff : (by : Shift from to) -> to = by.nat + from 0 shiftDiff : (by : Shift from to) -> to = by.nat + from
shiftDiff SZ = Refl shiftDiff SZ = Refl
shiftDiff (SS by) = cong S $ shiftDiff by shiftDiff (SS by) = cong S $ shiftDiff by

4
src/Quox/Syntax/Term.idr
View file

@ -332,10 +332,10 @@ parameters {auto _ : Alternative f}
upsilon1 (E e :# _) = pure e upsilon1 (E e :# _) = pure e
upsilon1 _ = empty upsilon1 _ = empty
public export export
step : Elim d n -> f (Elim d n) step : Elim d n -> f (Elim d n)
step e = betaLam1 e <|> upsilon1 e step e = betaLam1 e <|> upsilon1 e
public export export
step' : Elim d n -> Elim d n step' : Elim d n -> Elim d n
step' e = fromMaybe e $ step e step' e = fromMaybe e $ step e

2
src/Quox/Syntax/Var.idr
View file

@ -68,7 +68,7 @@ public export %inline
V : (i : Nat) -> {auto 0 p : i `LT` n} -> Var n V : (i : Nat) -> {auto 0 p : i `LT` n} -> Var n
V i {p} = fromNatWith i p V i {p} = fromNatWith i p
public export %inline export %inline
tryFromNat : Alternative f => (n : Nat) -> Nat -> f (Var n) tryFromNat : Alternative f => (n : Nat) -> Nat -> f (Var n)
tryFromNat n i = tryFromNat n i =
case i `isLT` n of case i `isLT` n of