package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/rocq-runtime.clib/Diff2/index.html

Module Diff2Source

An implementation of Eugene Myers' O(ND) Difference Algorithm[1]. This implementation is a port of util.lcs module of Gauche Scheme interpreter.

  • [1] Eugene Myers, An O(ND) Difference Algorithm and Its Variations, Algorithmica Vol. 1 No. 2, pp. 251-266, 1986.
Sourcetype 'a common = [
  1. | `Common of int * int * 'a
]

an element of lcs of seq1 and seq2

Sourcetype 'a edit = [
  1. | `Removed of int * 'a
  2. | `Added of int * 'a
  3. | 'a common
]

an element of diff of seq1 and seq2.

Sourcemodule type SeqType = sig ... end

Input signature of Diff.Make.

Sourcemodule type S = sig ... end

Output signature of Diff.Make.

Sourcemodule Make (M : SeqType) : S with type t = M.t and type elem = M.elem

Functor building an implementation of the diff structure given a sequence type.