package soteria

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

Module Value.Expr

Expr.t describes a syntactic representation of a value of type 'a v. Syntactic objects, unlike semantic values, can contain "free" variables and operations such as substitution have meaning.

Expr.t objects are used in, for instance, assertions (Logic). They can be substituted through a Producer monad or learned through a Consumer monad.

type t
val of_value : 'a t -> t

Obtain a syntactic representation from a semantic value. This implicitly uses an identity substitution.

val ty : t -> 'a ty

Gets the type associated to a syntactic values.

val subst : (t -> 'a t) -> t -> 'b t

Convenience function

module Subst : sig ... end

A susbtitution projects the syntactic to the semantic world.