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