ClaimAndUnfocus.idr

module ClaimAndUnfocus

foo : Nat -> Nat
foo = ?foo_rhs

---------- Proofs ----------

ClaimAndUnfocus.foo_rhs = proof
  claim bar Nat -> Nat -> Nat
  unfocus
  intro x
  exact bar x x
  intro x,y
  refine plus
  refine x
  refine y