Stream: Coq devs & plugin devs

Topic: insufficient types


view this post on Zulip Gaëtan Gilbert (Sep 14 2023 at 13:55):

When do we switch constr.t to intrisically typed syntax so that we may get type system guidance for debruijn manipulation?

view this post on Zulip Rodolphe Lepigre (Sep 14 2023 at 14:10):

Or you could move to bindlib and never think about debruijn manipulations ever again.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 14 2023 at 16:11):

Gaëtan Gilbert said:

When do we switch constr.t to intrisically typed syntax so that we may get type system guidance for debruijn manipulation?

This seems quite hard to do, isn't it?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 14 2023 at 16:12):

Rodolphe Lepigre said:

Or you could move to bindlib and never think about debruijn manipulations ever again.

That would be quite a undertaking ! It'd be quite interesting to see what the outcome is, in particular in terms of perfs

view this post on Zulip Pierre-Marie Pédrot (Sep 14 2023 at 16:13):

Terms are marshalled so they shouldn't rely on fancy tricks with uids and the like. The term AST is the basic type of the checker, so it should be as dumb as possible.

view this post on Zulip Pierre-Marie Pédrot (Sep 14 2023 at 16:13):

As for being sure we don't have a bug somewhere, that's why we have metacoq around.

view this post on Zulip Paolo Giarrusso (Sep 14 2023 at 17:58):

but metacoq won't help with a missing shift in a tactic, would it?


Last updated: Oct 13 2024 at 01:02 UTC