Zulip Chat Archive

Stream: new members

Topic: h : 5 = 4


view this post on Zulip Kevin Sullivan (Nov 17 2018 at 16:30):

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

view this post on Zulip Kenny Lau (Nov 17 2018 at 16:31):

what are the types?

view this post on Zulip 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

view this post on Zulip 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: May 14 2021 at 22:15 UTC