1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
------------------------------------------------------------------------
-- 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 1}} → ℕ → ℕ
inc {{step}} n = step .value + n
-- and indeed incrementing 2 gives you 3
_ : inc 2 ≡ 3
_ = refl
-- but you can also insist that you want to use a bigger increment by
-- passing the `step` argument explicitly
_ : inc {{10 !}} 2 ≡ 12
_ = refl
|
