toki/idris2-lens
1
0
Fork 0
Code Issues Pull requests Activity

Rename nil' to lin

Browse source
This commit is contained in:
Kiana Sheibani 2023-10-19 14:05:57 -04:00
parent ec451f0061
commit 4d44a6ac36
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Control/Lens/Cons.idr
View file

@ -67,5 +67,5 @@ last_ @{_} @{MkIsOptional _} = snoc_ . second
||| Use a `Snoc` implementation to construct an empty sequence. ||| Use a `Snoc` implementation to construct an empty sequence.
public export public export
nil' : Snoc s s a a => s lin : Snoc s s a a => s
nil' = review snocIso Nothing lin = review snocIso Nothing