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

i found an issue about that 0 bug

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

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

@ -102,7 +102,7 @@ toFromNat (S k) (LTESucc x) = cong S $ toFromNat k x
-- not using %transform like other things because weakSpec requires the proof -- 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 relevant. but since only `LTESucc` is ever possible that seems
-- to be a bug? -- to be an instance of <https://github.com/idris-lang/Idris2/issues/1259>?
export export
weak : (0 p : m `LTE` n) -> Var m -> Var n 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 {rel=LTE}