Open hargoniX opened 6 months ago
@nomeata conjectures that this is because autoImplicit variables are inserted at the beginning of the arguments list which makes it impossible to model the dependency on decl.
Correct.
Another possible workaround it to use auto implicit for decls
too.
theorem go_foo' (x : Nat) : go decls h = true := sorry
Prerequisites
Description
This code throws an error in the theorem statement of
go_foo
while trying to figure out the correct type forh
:which is rather surprising given that there are mvars on the one side and concrete values on the other side. The error can be fixed by changing the theorem statement as follows:
@nomeata conjectures that this is because
autoImplicit
variables are inserted at the beginning of the arguments list which makes it impossible to model the dependency ondecl
.Context
In my practical code the statement behind
h
is large so I would like to avoid writing it out, while I can manage to do that with the mentioned workaround it would be nice if we had better UX here.Expected behavior: If Joachim is right, either addressing this issue to allow for such
autoImplicit
s or producing a more reasonable error for a user is probably the way to go.Actual behavior: Confusing mvar error.
Versions
"4.7.0-rc2"
Impact
Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.