Mentions légales du service

Skip to content

Add support for recursive record definitions

Armaël Guéneau requested to merge agueneau/cfml:recursive-records-2 into master

This adds support for the following code, which is useful e.g. when implementing doubly linked lists:

type node = { mutable prev : node; mutable next : node }
let create_node () : node =
  let rec node = { prev = node; next = node } in
  node

There's a small demo added in examples/Tuto/Demo_proof.v.

Merge request reports

Loading