mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-28 02:23:44 +03:00
3e0d5acfa4
The proofs of depth-invariance for Always Until and Exists Until require mapping the proofs over the Formulae's internal `All` and `Any` respectively. Idris provides some functions for this, but they erase the list and so don't quite work. Instead we need to implement our own, which don't erase the list. |
||
---|---|---|
.. | ||
base | ||
contrib | ||
linear | ||
network | ||
papers | ||
prelude | ||
test |