------------------------------------------------------------------------
-- The Agda standard library
--
-- An example showing how to define a function taking an optional
-- argument that default to a specified value if none is passed.
------------------------------------------------------------------------

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

module README.Data.Default where

open import Data.Default
open import Data.Nat.Base hiding (_!)
open import Relation.Binary.PropositionalEquality

-- 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

-- Note that you will only get this behaviour if the `default` instance
-- is in scope so you should either import `Data.Default` in your client
-- modules or publicly re-export the type and the instance!

-- `inc` increments its argument by the value `step`, defaulting to 1
inc : {{step : WithDefault }} → ℕ → ℕ
inc {{step}} n = step .value + n

-- and indeed incrementing 2 gives you 3
_ : inc  ≡ 
_ = refl

-- but you can also insist that you want to use a bigger increment by
-- passing the `step` argument explicitly
_ : inc {{ !}}  ≡ 
_ = refl