idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-01 09:49:24 +03:00
Code Issues Projects Releases Wiki Activity

Proof of list bounds was made to be not present at runtime when indexing

Browse Source
This commit is contained in:
Denis Buzdalov 2020-12-03 17:26:05 +03:00 committed by G. Allais
parent 57a8ef4609
commit f2596318e5
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libs/base/Data/List.idr
View File

@ -58,7 +58,7 @@ inBounds (S k) (x :: xs) with (inBounds k xs)
|||
||| @ ok a proof that the index is within bounds
public export
index : (n : Nat) -> (xs : List a) -> {auto ok : InBounds n xs} -> a
index : (n : Nat) -> (xs : List a) -> {auto 0 ok : InBounds n xs} -> a
index Z (x :: xs) {ok = InFirst} = x
index (S k) (_ :: xs) {ok = InLater _} = index k xs