Elaborating With

With.agda

module With where

open import Data.Nat using (ℕ ; _+_)
open import Relation.Binary.PropositionalEquality

module UsingWith where
  
  plus-n-0 : (n : ℕ) → n + 0 ≡ n
  plus-n-0 ℕ.zero    = refl
  plus-n-0 (ℕ.suc n) with n + 0 | plus-n-0 n
  plus-n-0 (ℕ.suc n) | .n | refl = refl

module ElabWith where

mutual

  plus-n-0 : (n : ℕ) → n + 0 ≡ n
  plus-n-0 ℕ.zero    = refl
  plus-n-0 (ℕ.suc n) = plus-n-0-with n (n + 0) (plus-n-0 n)

  plus-n-0-with : (n k : ℕ) → k ≡ n → ℕ.suc k ≡ ℕ.suc n
  plus-n-0-with _ _ refl = refl