comment out an unfinished definition lmao
This commit is contained in:
parent
b1699ce022
commit
415a823dec
1 changed files with 3 additions and 0 deletions
|
@ -149,6 +149,8 @@ def0 times-zero : (m : ℕ) → 0 ≡ timesω m 0 : ℕ =
|
|||
succ m', ih ⇒ ih
|
||||
};
|
||||
|
||||
{-
|
||||
-- unfinished
|
||||
def0 times-succ : (m n : ℕ) → plus m (timesω m n) ≡ timesω m (succ n) : ℕ =
|
||||
λ m n ⇒
|
||||
case m
|
||||
|
@ -158,5 +160,6 @@ def0 times-succ : (m n : ℕ) → plus m (timesω m n) ≡ timesω m (succ n) :
|
|||
succ m', ih ⇒
|
||||
δ 𝑖 ⇒ plus (succ n) (ih @𝑖)
|
||||
};
|
||||
-}
|
||||
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue