mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-01 01:09:03 +03:00
[ lint ] this is so silly
This commit is contained in:
parent
f04a29926d
commit
9aa9e98a35
@ -134,7 +134,7 @@
|
||||
* Adds `Data.Fin.finToNatEqualityAsPointwise`,
|
||||
which takes a witness of `finToNat k = finToNat l` and proves `k ~~~ l`.
|
||||
* Drop first argument (path to the `node` executable) from `System.getArgs` on
|
||||
the node backend to make it consistent with other backends.
|
||||
the Node.js backend to make it consistent with other backends.
|
||||
|
||||
#### Test
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user