------------------------------------------------------------------------
-- The Agda standard library
--
-- A way to specify that a function's argument takes a default value
-- if the argument is not passed explicitly.
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Default where

-- An argument of type `WithDefault {a} {A} x` is an argument of type
-- `A` that happens to default to `x` if no other value is specified
-- (as long as the `default` instance is in scope)

infixl  _!
record WithDefault {a} {A : Set a} (x : A) : Set a where
  constructor _!
  field value : A
open WithDefault public

instance
  default : ∀ {a} {A : Set a} {x : A} → WithDefault x
  default {x = x} .value = x

-- See README.Data.Default for an example