We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
On the branch issabelle2017, when I run
issabelle2017
<somewhere where Isabelle2017 was extracted>/Isabelle2017/bin/isabelle build -d . simplewallet
I see
*** Failed to load theory "simplewallet.Apply_Trace_Cmd" (unresolved "simplewallet.Apply_Trace") *** Failed to load theory "simplewallet.Hoare" (unresolved "simplewallet.Apply_Trace_Cmd") *** ML error (line 119 of "~/src/eth-isabelle/attic/Apply_Trace.thy"): *** Type of function does not match type of recursive application. *** Function: *** fun *** proof_body_descend' f get_fact ... *** = *** (if ... ... then (... handle ...) else raise ...) *** handle Option => (... handle ...) *** : ('a -> bool) -> *** ('a -> 'b option) -> *** Inttab.key * ('a * 'c * proof_body future) -> *** ('a * 'b) option Inttab.table -> ('a * 'b) option Inttab.table *** Variable: proof_body_descend' : *** ('a -> bool) -> *** ('a -> 'b option) -> *** serial * thm_node -> *** ('a * 'b) option Inttab.table -> ('a * 'b) option Inttab.table *** Reason: *** Can't unify thm_node to 'a * 'b * proof_body future *** (Incompatible types) *** At command "ML" (line 18 of "~/src/eth-isabelle/attic/Apply_Trace.thy") Unfinished session(s): simplewallet 0:02:10 elapsed time, 0:03:35 cpu time, factor 1.65
The text was updated successfully, but these errors were encountered:
@seed told me a workaround: replacing apply_trace with apply.
apply_trace
apply
Sorry, something went wrong.
No branches or pull requests
On the branch
issabelle2017
, when I runI see
The text was updated successfully, but these errors were encountered: