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

add lengthPrf0 for contexts

Browse source
This commit is contained in:
rhiannon morris 2021-12-23 16:03:49 +01:00
parent 7bc58625a1
commit 1924250fcd
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Quox/Context.idr
View file

@ -183,6 +183,12 @@ lengthPrf [<] = (0 ** Refl)
lengthPrf (tel :< _) = lengthPrf (tel :< _) =
let len = lengthPrf tel in (S len.fst ** cong S len.snd) let len = lengthPrf tel in (S len.fst ** cong S len.snd)
export
lengthPrf0 : Context _ to -> (len : Nat ** len = to)
lengthPrf0 ctx =
let (len ** prf) = lengthPrf ctx in
(len ** rewrite sym $ plusZeroRightNeutral len in prf)
public export %inline public export %inline
length : Telescope {} -> Nat length : Telescope {} -> Nat
length = fst . lengthPrf length = fst . lengthPrf