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