packages feed

Agda-2.3.2.2: notes/papers/implicit/examples/Simple.agda

module Simple where

postulate
  Nat  : Set
  zero : Nat

  -- we want
  -- ?0 zero = zero
  -- and then
  -- ?0 x = x