on 1b71663 help sign in
2 files
../ Quantifiers.idrChange export qualifier keywords Views.idrmark covering functions using `sizeAccessible` as `public export total` so that they reduce in proofs