Тут только не веб программисты

Ого

Кто в курсе как фиксить вот такую хуйню при записи макроса

Блять, у меня мозг треснул

Решил с Isabelle/HOL поиграться.

theory Sub
imports Main
begin

fun sub :: "nat ⇒ nat ⇒ nat"
  where 
    "sub 0 m = 0" |
    "sub n 0 = n" |
    "sub (Suc n) (Suc m) = sub n m"

lemma[simp]: "sub 0 m ≡ 0"
  by simp

lemma[simp]: "sub n 0 = n"
  apply (induction n)
   apply auto
  done

lemma[simp]: "sub m m = 0"
  apply (induction m)
   apply auto
  done

lemma[simp]: "sub n (Suc 0) = n - Suc 0"
  apply (induction n)
   apply auto
  done


end

Три утверждения я доказал, ещё 2 не могу, что для любого m >= n результат 0, и для любого m < n результат n - m

Там пишет, что запись не возможна

Это ебать что

Вот в упор не могу понять, как на натуральных числах доказать, что m > n => n - m

Прувер

Позволяет математические доказательства писать

Нифига

Прикольно

Ахуенное утверждение

Вот пример с умножением натуральных чисел:

theory Mul
imports Main
begin

fun mul :: "nat ⇒ nat ⇒ nat"
  where 
    "mul n 0 = 0" |
    "mul n (Suc(m)) = n + mul n m"


lemma[simp]: "mul 0 m = 0"
  apply (induction m)
   apply auto
  done


lemma[simp]: "mul (Suc n) m = m + n * m"
  apply (induction m)
   apply auto
  done

lemma "mul n m = n * m"
  apply (induction n)
   apply auto
  done


end

Так оно на бекенде дёгает Z3

Если м больше н вычту н из м

Там используются cvc4 z3 spass e

так ты это машине объясни