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

remove an (.int). no one likes ints

Browse source
This commit is contained in:
rhiannon morris 2021-09-03 17:54:52 +02:00
parent 6c05a348d5
commit 6da33625f8
2 changed files with 4 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -277,10 +277,14 @@ NotCloTerm d n = Subset (Term d n) $ So . not . isCloT
mutual
||| if the input term has any top-level closures, push them under one layer of
||| syntax
export
pushSubstsT : Term d n -> NotCloTerm d n
pushSubstsT s = pushSubstsT' id id s
||| if the input elimination has any top-level closures, push them under one
||| layer of syntax
export
pushSubstsE : Elim d n -> NotCloElim d n
pushSubstsE e = pushSubstsE' id id e

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

@ -99,14 +99,6 @@ toFromNat 0 (LTESucc x) = Refl
toFromNat (S k) (LTESucc x) = cong S $ toFromNat k x
public export
(.int) : Var n -> Integer
i.int = natToInteger i.nat
%builtin NaturalToInteger Var.(.int)
public export Cast (Var n) Integer where cast i = i.int
-- not using %transform like other things because weakSpec requires the proof
-- to be relevant. but since only `LTESucc` is ever possible that seems
-- to be a bug?