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

use Subset instead of relevant product

Browse source
This commit is contained in:
rhiannon morris 2022-04-11 23:34:28 +02:00
parent d912614d7d
commit 7faca8ac27
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Quox/Context.idr
View file

@ -196,16 +196,16 @@ zipWith3Lazy f = zipWith3 $ \x, y, z => delay $ f x y z
export
lengthPrf : Telescope _ from to -> (len : Nat ** len + from = to)
lengthPrf [<] = (0 ** Refl)
lengthPrf : Telescope _ from to -> Subset Nat (\len => len + from = to)
lengthPrf [<] = Element 0 Refl
lengthPrf (tel :< _) =
let len = lengthPrf tel in (S len.fst ** cong S len.snd)
let len = lengthPrf tel in Element (S len.fst) (cong S len.snd)
export
lengthPrf0 : Context _ to -> (len : Nat ** len = to)
lengthPrf0 : Context _ to -> Subset Nat (\len => len = to)
lengthPrf0 ctx =
let (len ** prf) = lengthPrf ctx in
(len ** rewrite sym $ plusZeroRightNeutral len in prf)
let len = lengthPrf ctx in
Element len.fst (rewrite sym $ plusZeroRightNeutral len.fst in len.snd)
public export %inline
length : Telescope {} -> Nat