Stream: Equations devs & users

Topic: Difference noconf H et depelim H


view this post on Zulip Thomas Lamiaux (Oct 07 2024 at 17:34):

What is the difference between the tactic noconf H et depelim H ?

view this post on Zulip Théo Winterhalter (Oct 07 2024 at 18:04):

noconf will work on an equality while depelim on anything of inductive type?

view this post on Zulip Matthieu Sozeau (Oct 08 2024 at 12:42):

Essentially, yes


Last updated: Oct 13 2024 at 01:02 UTC