Zulip Chat Archive

Stream: general

Topic: This will brick your computer!

Kenny Lau (Sep 14 2018 at 10:33):

import data.int.basic
set_option trace.class_instances true
#check λ n : ℤ, (n : ℕ)

Kevin Buzzard (Sep 14 2018 at 11:11):

This is well known. Lean will time out trying to coerce an int into a nat rather than give up

Kenny Lau (Sep 14 2018 at 11:12):

remove the first line and it's fine!

Kevin Buzzard (Sep 14 2018 at 11:12):

Hopefully fixed in Lean 4

Kenny Lau (Sep 17 2018 at 06:21):

import data.polynomial

universe u

variables {α : Type u} [comm_semiring α] [decidable_eq α]

def derivative (p : polynomial α) : polynomial α :=
finsupp.sum p $ λ n c, n * polynomial.C c * polynomial.X^(n-1)

@[simp] lemma derivative_C_mul_X (x : α) (n : ℕ) :
  derivative (polynomial.C x * polynomial.X^n) = n * polynomial.C x * polynomial.X^(n-1) :=
begin
  unfold derivative,
  rw [← polynomial.single_eq_C_mul_X, finsupp.sum_single_index],
  all_goals { rw [polynomial.C_0, mul_zero, zero_mul] }
end

--timeout
@[simp] lemma derivative_C (x : α) :
  derivative (polynomial.C x) = 0 :=
derivative_C_mul_X x 0