on 90ae69b help sign in
1 file
../ Views.idrmark covering functions using `sizeAccessible` as `public export total` so that they reduce in proofs