Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Default named arguments
record Default {ℓ} (A : Set ℓ) (a : A) : Setwhere
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 34
_ = refl
_ : incr 3 {{steps = 2 !}} ≡ 5
_ = refl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment