packages feed

agda-unused-0.2.0: data/expression/Lam.agda

module Lam where

f
  : {A : Set}
  → A
  → A
f x
  = (λ y z → z) x x

g
  : {A : Set}
  → A
  → A
g {A = A} x
  = (λ (y' : A) (z : A) → z) x x