Zulip Chat Archive
Stream: mathlib4
Topic: Invalid auto and opt values
Matthew Ballard (Jan 19 2023 at 17:24):
def num : Nat := 5
theorem is_five : num = 5 := by rfl
class test where
numb : Nat := num
isFive : numb = 5 := by apply is_five
complains invalid auto tactic, identifier is not allowed
.
Breaking := by
with parentheses
def num : Nat := 5
theorem is_five : num = 5 := by rfl
class test where
numb : Nat := num
isFive : numb = 5 := (by apply is_five)
now gives tactic ‘apply’ failed, failed to unify num = 5 with numb = 5
This works
def num : Nat := 5
theorem is_five : num = 5 := by rfl
class test where
numb : Nat := num
isFive : numb = 5 := by rfl
but this does not
def num : Nat := 5
theorem is_five : num = 5 := by rfl
class test where
numb : Nat := num
isFive : numb = 5 := (by rfl)
It seems the we lose contact with the other opt value with the parentheses.
Is the current solution to write a throwaway tactic to avoid the parentheses?
Last updated: Dec 20 2023 at 11:08 UTC