Default named arguments

DefaultArgument.agda

record Default {ℓ} (A : Set ℓ) (a : A) : Set ℓ where
  constructor _!
  field value : A

instance

  default : ∀ {ℓ} {A : Set ℓ} a → Default A a
  default a = record { value = a }

open import Agda.Builtin.Nat

incr : Nat → {{steps : Default Nat 1}} → Nat
incr n {{steps}} = Default.value steps + n

open import Relation.Binary.PropositionalEquality

_ : incr 3 ≡ 4
_ = refl

_ : incr 3 {{steps = 2 !}} ≡ 5
_ = refl