search

rems-project / lem

Lem semantic definition language
Other
130 stars 15 forks source link

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

Open bacam opened 6 years ago

bacam commented 6 years ago

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.