linksem
  1. Overview
  2. Docs
package linksem
Legend:
Library
Module
Module type
Parameter
Class
Class type
type binary_relation =
  1. | Eq0
  2. | Lt0
type binary_connective =
  1. | And0
  2. | Or0
type expression =
  1. | Var0 of string
  2. | Const of Nat_big_num.num
type value_formula =
  1. | VFTrue
  2. | VFFalse
  3. | VFBinaryRelation of binary_relation * expression
  4. | VFBinaryConnective of binary_connective * value_formula * value_formula
  5. | VFNot of value_formula
type memory_image_formula =
  1. | MIFTrue
  2. | MIFFalse
  3. | MIFExists of string * memory_image_formula
  4. | MIFBinaryRelation of binary_relation * expression * expression
  5. | MIFBinaryConnective of binary_connective * memory_image_formula * memory_image_formula
  6. | MIFAssertValueFormula of expression * value_formula
  7. | MIFNot of memory_image_formula
type memory_image0 =
  1. | MemoryImage of memory_image_formula