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: Dec 20 2023 at 11:08 UTC