
  0 | module Language.Implicits.IfUnsolved
  1 | 
  2 | %default total
  3 | 
  4 | ||| Interface for providing default value for an implicit in case of unsolved hole.
  5 | |||
  6 | ||| Once you have an implicit argument `e` that in some contexts can be determined by
  7 | ||| other arguments and/or return value, and one some contexts cannot, you can add
  8 | ||| a constraint `IfUnsolved val e =>` to a function to make `e` be chosen to be `val`
  9 | ||| *only in cases* when in either way `e` would be an unsolved hole.
 10 | |||
 11 | ||| The `IfUnsolved val e` works nicely even if this parameter is of quantity `0`.
 12 | export
 13 | interface IfUnsolved (0 def, a : ty) where
 14 |   constructor MkIfUnsolved
 15 | 
 16 | export %defaulthint
 17 | TheIfUnsolved : IfUnsolved x x
 18 | TheIfUnsolved = MkIfUnsolved
 19 | 
 20 | export
 21 | IfUnsolved def x where
 22 |