When do we switch constr.t to intrisically typed syntax so that we may get type system guidance for debruijn manipulation?
Or you could move to bindlib and never think about debruijn manipulations ever again.
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?
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
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.
As for being sure we don't have a bug somewhere, that's why we have metacoq around.
but metacoq won't help with a missing shift in a tactic, would it?
Last updated: Oct 13 2024 at 01:02 UTC