mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-26 21:23:53 +03:00
9 lines
288 B
Plaintext
9 lines
288 B
Plaintext
1/1: Building LCase (LCase.idr)
|
|
LCase.idr:7:11--10:13:While processing right hand side of foo at LCase.idr:6:1--12:1:
|
|
There are 0 uses of linear name y at:
|
|
7 = let 1 test = the Nat $ case z of
|
|
8 Z => Z
|
|
9 (S k) => S z
|
|
10 in
|
|
|