integrate binders in def #46

New issue

Open

opened 2024-05-10 19:57:31 +02:00 by rhi · 0 comments

rhi commented

2024-05-10 19:57:31 +02:00

Owner

this kinda thing

-- old:                         -- new:
def plus : ℕ → ℕ → ℕ =          def plus (m n : ℕ) : ℕ =
  λ m n ⇒                          case m return ℕ of {
  case m return ℕ of {               zero      ⇒ n;
    zero      ⇒ n;                   succ _, p ⇒ succ p
    succ _, p ⇒ succ p             }
  }

maybe also allow the return type to be synthed if the body is an elim

this kinda thing ``` -- old: -- new: def plus : ℕ → ℕ → ℕ = def plus (m n : ℕ) : ℕ = λ m n ⇒ case m return ℕ of { case m return ℕ of { zero ⇒ n; zero ⇒ n; succ _, p ⇒ succ p succ _, p ⇒ succ p } } ``` maybe also allow the return type to be synthed if the body is an elim