See line 93 in the screenshot below:
When solving the proof, eventually the conclusion reaches:
and the current implementation breaks, as it tries to apply the constructors for line 94.
Note: This is a separate issue to the current restriction we have to use the plugin wherein we do not allow for terms to be assigned in premises, e.g., if a function determines the resulting term then the function must be called in the resulting term.
Proposed Solution
It would be most convenient if we collect the information of any premises that are non-lts as we are building the initial LTS-graph. Such premises are encountered within Rocq_monad_utils.Unification.check_updated_ctx, after match F.find_opt indmap name with | None ->. Although, ideally we would collect this information with the Rocq_monad_utils.Bindings/ConstructorBindings, so that the Model.Info.Meta.RocqLTS.t contains this and is easily accessible by the ProofSolver
See line
93in the screenshot below:When solving the proof, eventually the conclusion reaches:
and the current implementation breaks, as it tries to apply the constructors for line
94.Proposed Solution
It would be most convenient if we collect the information of any premises that are non-lts as we are building the initial LTS-graph. Such premises are encountered within
Rocq_monad_utils.Unification.check_updated_ctx, aftermatch F.find_opt indmap name with | None ->. Although, ideally we would collect this information with theRocq_monad_utils.Bindings/ConstructorBindings, so that theModel.Info.Meta.RocqLTS.tcontains this and is easily accessible by theProofSolver