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

add casts to Integer for Var & Shift

Browse source
This commit is contained in:
rhiannon morris 2022-02-27 01:36:08 +01:00
parent 610b5fde2d
commit 9b260529c8
2 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -23,7 +23,8 @@ public export
(SS by).nat = S by.nat
%transform "Shift.(.nat)" Shift.(.nat) = believe_me
public export Cast (Shift from to) Nat where cast = (.nat)
public export Cast (Shift from to) Nat where cast = (.nat)
public export Cast (Shift from to) Integer where cast = cast . cast {to = Nat}
export Eq (Shift from to) where (==) = (==) `on` (.nat)
export Ord (Shift from to) where compare = compare `on` (.nat)

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

@ -23,7 +23,8 @@ public export
(VS i).nat = S i.nat
%transform "Var.(.nat)" Var.(.nat) i = believe_me i
public export Cast (Var n) Nat where cast n = n.nat
public export Cast (Var n) Nat where cast = (.nat)
public export Cast (Var n) Integer where cast = cast . cast {to = Nat}
export Eq (Var n) where i == j = i.nat == j.nat
export Ord (Var n) where compare i j = compare i.nat j.nat