01-arguments.agda

-- {-# OPTIONS --verbose tc.constr.findInScope:15 #-}

module 01-arguments where

data T : Set where
  tt : T

data A : Set where
  mkA : A
  mkA2 : T → A

giveA : ⦃ a : A ⦄ → A
giveA {{a}} = a

test : A → T
test a = tt

test2 : T
test2 = test giveA

id : {A : Set} → A → A
id v = v

test5 : T → T
test5 = id

⋯ : {A : Set} → {{a : A}} → A
⋯ {{a}} = a

--giveA' : {{a : A}} → A
--giveA' = ⋯