Skip to content
New issue

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

Multiple let ... and ... clauses allowed for same function, but output doesn't work in OCaml/Coq #2

Open
bacam opened this issue Feb 26, 2018 · 0 comments

Comments

@bacam
Copy link
Contributor

bacam commented Feb 26, 2018

The following function definition (from Sail) typechecks and produces useful output for Isabelle/HOL and HOL4, but not OCaml or Coq:

val foreach : forall 'a 'vars.
  (list 'a) -> 'vars -> ('a -> 'vars -> 'vars) -> 'vars
let rec foreach [] vars _ = vars
and foreach (x :: xs) vars body = foreach xs (body x vars) body

The resulting code for OCaml and Coq has the same structure, which they don't allow (the clauses have to define different functions), whereas the HOLs get the obvious equations. I'm not sure if we ought to reject this in typechecking or translate it into a supported pattern match.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant