agda-unused-0.2.0: data/declaration/TypeSig.agda
module Definition where
f
: {A : Set}
→ A
→ A
f x
= x
g
: {A : Set}
→ A
→ A
g x
= x
h
: {A : Set}
→ A
→ A
h x
= f x
_
: {A : Set}
→ A
→ A
_
= λ x → x
module Definition where
f
: {A : Set}
→ A
→ A
f x
= x
g
: {A : Set}
→ A
→ A
g x
= x
h
: {A : Set}
→ A
→ A
h x
= f x
_
: {A : Set}
→ A
→ A
_
= λ x → x