gog.agda

module gog where

open import Data.Sum
open import Function
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning


data ℕ : Set where
  z : ℕ
  s : ℕ → ℕ

infixl 6 _+_
_+_ : ℕ → ℕ → ℕ
z   + n = n
s m + n = s (m + n)


infixl 7 _*_
_*_ : ℕ → ℕ → ℕ
z   * _ = z
s m * n = n + m * n

-- decided to write own ones because why not


--infixr 8 _^_,_
-- _^_,_ : ∀ m n → m ≢ z ⊎ n ≢ z → ℕ
-- m ^ z   , inj₁ m≠z = s z
-- m ^ s n , inj₁ m≠z = m * m ^ n , inj₁ m≠z
-- z ^ n   , inj₂ n≠z = z
-- s m ^ n , inj₂ n≠z = n * m ^ n , inj₂ n≠z


data OnlyOneZero : ℕ → ℕ → Set where
  instance
    left : ∀{m n} → OnlyOneZero (s m) n
    right :  ∀{m n} → OnlyOneZero m (s n)

infixr 8 _^_
_^_ : ∀ m n {{p : OnlyOneZero m n}} → ℕ
z ^ s n = z
s m ^ z = s z
s m ^ s n = s m * (s m ^ n)


-- I tried to implent ^ with implicit `m ≢ z ⊎ n ≢ z`, because with explicit one pattern-matching would be ugly
-- v v v
-- ^2-* : ∀ n {p} → n * n ≡ n ^ s (s z) , p
-- ^2-* z {inj₁ x} = refl --  ugly
-- ^2-* z {inj₂ y} = refl --  ...
-- ^2-* (s n) = {!   !}