Zulip Chat Archive

Stream: general

Topic: A strange bug in elaborator

Yury G. Kudryashov (Jan 14 2021 at 19:58):

In branch#open-map, I get a strange error: after refine open_map_of_strict_fderiv (λ x, (hf x).has_strict_fderiv_at_equiv _), here, there is no x in the proof state.

Yury G. Kudryashov (Jan 14 2021 at 19:59):

CI gives this error: https://github.com/leanprover-community/mathlib/runs/1704114619

Eric Wieser (Jan 14 2021 at 20:05):

In context: https://github.com/leanprover-community/mathlib/compare/open-map#diff-4882f676fe5e32ba0843bce0892c50c82525b538ffabcc12fc73a4e6e2d13b04R523

Yury G. Kudryashov (Jan 14 2021 at 20:44):

I tried to write a term mode proof open_map_of_strict_fderiv (λ x, (hf x).has_strict_fderiv_at_equiv (h0 x)) but it fails as well.

Last updated: Dec 20 2023 at 11:08 UTC