Idris2Doc : Language.Reflection.Refined.Util

Language.Reflection.Refined.Util

(source)
Utilities for Language.Reflection.Refined

Reexports

import public Data.Maybe
import public Data.So

Definitions

maybeSo : (b : Bool) -> Maybe (So b)
  Try and convert a boolean to `So`, that is, a proof that the
  boolean in question equals `True`.

Totality: total
Visibility: public export
refineSo : {f : a -> Bool} -> ((v : a) -> (0 _ : So (f v)) -> b) -> a -> Maybe b
  Try to create a refined value that requires an erased proof of `So (f v)`.

Totality: total
Visibility: public export