Zulip Chat Archive

Stream: new members

Topic: h : 5 = 4

Kevin Sullivan (Nov 17 2018 at 16:30):

Dumb question: How do I get false from a hypothesis, 5 = 4? Syntax thing.

Kenny Lau (Nov 17 2018 at 16:31):

what are the types?

Kenny Lau (Nov 17 2018 at 16:33):

import data.real.basic tactic.norm_num

example (h : (5:ℕ) = 4) : false := by cases h
example (h : (5:ℤ) = 4) : false := by cases h
example (h : (5:ℚ) = 4) : false := by norm_num at h
example (h : (5:ℝ) = 4) : false := by norm_num at h

Kevin Sullivan (Nov 17 2018 at 16:34):

import data.real.basic tactic.norm_num

example (h : (5:ℕ) = 4) : false := by cases h
example (h : (5:ℤ) = 4) : false := by cases h
example (h : (5:ℚ) = 4) : false := by norm_num at h
example (h : (5:ℝ) = 4) : false := by norm_num at h

Ah, thank you, Kenny.

Last updated: Dec 20 2023 at 11:08 UTC