Zulip Chat Archive

Stream: mathlib4

Topic: nontriviality leaves metavars


Yury G. Kudryashov (Jan 22 2023 at 17:57):

Hi, the following code in Data.Set.Finite leaves metavariables:

example : Finite α := by
  show_term { nontriviality α; sorry }

Yury G. Kudryashov (Jan 22 2023 at 18:00):

In Lean 3, I get

Try this: refine (subsingleton_or_nontrivial α).dcases_on (λ (_inst : subsingleton α), finite.of_subsingleton)
  (λ (_inst : nontrivial α),
     _[subsingleton_or_nontrivial α, subsingleton_or_nontrivial α, subsingleton_or_nontrivial α, _inst])

Yury G. Kudryashov (Jan 22 2023 at 18:00):

BTW, why are there 3 subsingleton_or_nontrivial α in the output?

Yury G. Kudryashov (Jan 22 2023 at 18:19):

@Sebastien Gouezel @Mario Carneiro You're the authors of nontriviality in Mathlib 4 :up:

Mario Carneiro (Jan 22 2023 at 21:04):

The core issue is lean4#2054, I posted a workaround in mathlib4#1769

Yury G. Kudryashov (Jan 22 2023 at 23:07):

Could you add a test, please?


Last updated: Dec 20 2023 at 11:08 UTC