Zulip Chat Archive

Stream: new members

Topic: Documentation of unification hints


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Jul 07 2020 at 13:22):

Thanks!

view this post on Zulip Patrick Massot (Jul 07 2020 at 13:22):

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

view this post on Zulip Patrick Massot (Jul 07 2020 at 13:22):

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


Last updated: May 08 2021 at 03:17 UTC