Zulip Chat Archive

Stream: new members

Topic: Documentation of unification hints

Enrico Tassi (Jul 07 2020 at 13:18):

Hello, I'm new here. I was looking at the syntax to declare unification hints but I could not find it in the documentation. Can someone hand me a pointer?

Patrick Massot (Jul 07 2020 at 13:19):

Hi! You should ask Assia and Cyril their Amsterdam demo file. As far as I know, they are the only users of unification hints in Lean.

Johan Commelin (Jul 07 2020 at 13:20):

This might be the best we have: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/unification.20hints/near/158607080

Patrick Massot (Jul 07 2020 at 13:22):

Also a coupe of tests at https://github.com/leanprover-community/lean/blob/master/tests/lean/run/unification_hints.lean and surrounding files maybe.

Enrico Tassi (Jul 07 2020 at 13:22):

Thanks!

Patrick Massot (Jul 07 2020 at 13:22):

Nice, Johan's answer is a more efficient version of my answer.

Patrick Massot (Jul 07 2020 at 13:22):

(featuring links to Assia and Cyril's files).

Last updated: Dec 20 2023 at 11:08 UTC