Zulip Chat Archive

Stream: lean4

Topic: tactic termination checking doesn't work for indexed types

Jad Ghalayini (Dec 03 2021 at 20:53):

See my issue @ https://github.com/leanprover/lean4/issues/848

Last updated: Feb 28 2026 at 14:05 UTC