package jasmin

  1. Overview
  2. Docs
package jasmin
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Jasmin.Values

val undef_t : Type.stype -> Type.stype
type value =
  1. | Vbool of bool
  2. | Vint of BinNums.coq_Z
  3. | Varr of BinNums.positive * Warray_.WArray.array
  4. | Vword of Wsize.wsize * Ssralg.GRing.ComRing.sort
  5. | Vundef of Type.stype
val undef_v : Type.stype -> value
val undef_addr : Type.stype -> value
type values = value list
val is_defined : value -> bool
val type_of_val : value -> Type.stype
val coq_DB : bool -> value -> bool
val to_bool : value -> (Utils0.error, bool) Utils0.result
val to_val : Type.stype -> Sem_type.sem_t -> value
val oto_val : Type.stype -> Sem_type.sem_ot -> value
val truncate_val : Type.stype -> value -> value Utils0.exec
val list_ltuple : Type.stype list -> Sem_type.sem_tuple -> values
val app_sopn : Type.stype list -> 'a1 Utils0.exec Sem_type.sem_prod -> value list -> 'a1 Utils0.exec