File: instr.mli

package info (click to toggle)
coq-doc 8.20.0-2
  • links: PTS, VCS
  • area: non-free
  • in suites: forky, sid, trixie
  • size: 46,708 kB
  • sloc: ml: 234,429; sh: 4,686; python: 3,359; ansic: 2,644; makefile: 842; lisp: 172; javascript: 87; xml: 24; sed: 2
file content (18 lines) | stat: -rw-r--r-- 1,181 bytes parent folder | download | duplicates (2)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(** Platform-specific Implementation of a global instruction counter. *)

(** [read_counter ()] returns the current value of the instruction counter, or
    an error message indicating why it could not be obtained. Note that counts
    returned by this function are not meaningful in absolute terms. To measure
    how many instructions it takes to run a piece of code, read the counter at
    the start and at the end, and compute the difference. *)
val read_counter : unit -> (Int64.t, string) Result.t