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: May 02 2025 at 03:31 UTC