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

add %inline to some instances

Browse source
This commit is contained in:
rhiannon morris 2022-02-27 01:47:55 +01:00
parent 76c02adf03
commit 7d821b20ef
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -23,12 +23,12 @@ public export
(VS i).nat = S i.nat (VS i).nat = S i.nat
%transform "Var.(.nat)" Var.(.nat) i = believe_me i %transform "Var.(.nat)" Var.(.nat) i = believe_me i
public export Cast (Var n) Nat where cast = (.nat) public export %inline Cast (Var n) Nat where cast = (.nat)
public export Cast (Var n) Integer where cast = cast . cast {to = Nat} public export %inline Cast (Var n) Integer where cast = cast . cast {to = Nat}
export Eq (Var n) where i == j = i.nat == j.nat export %inline Eq (Var n) where i == j = i.nat == j.nat
export Ord (Var n) where compare i j = compare i.nat j.nat export %inline Ord (Var n) where compare i j = compare i.nat j.nat
export Show (Var n) where showPrec d i = showCon d "V" $ showArg i.nat export %inline Show (Var n) where showPrec d i = showCon d "V" $ showArg i.nat
parameters {auto _ : Pretty.HasEnv m} parameters {auto _ : Pretty.HasEnv m}