package gospel

You can search for identifiers within the package.

in-package search v0.2.0

package gospel

gospel
- Gospel
  - Coercion
  - Dterm
    
    Mstr
  - Gospelstdlib
  - Identifier
    
    Ident
    
    Preid
  - Opprintast
  - Parser_frontend
  - Pps
  - Tast
  - Tast_helper
  - Tast_printer
  - Tmodule
    
    Mid
    
    Mstr
  - Tterm
    
    LS
    
    Mls
    
    Sls
    
    Svs
    
    Vs
  - Ttypes
    
    Htv
    
    Mts
    
    Mtv
    
    Mxs
    
    Ts
    
    Tvar
    
    Xs
  - Typing
  - Uast
  - Uattr2spec
  - Ulexer
  - Uparser
  - Upretty_printer
  - Utils
    
    Fmt
    
    Sstr

Legend:
Library
Module
Module type
Parameter
Class
Class type

type t

a set of coercions

val empty : t

val add : t -> Tterm.lsymbol -> t

adds a new coercion from function ls: ty1 -> ty2 raises an error if

this introduces a cycle, i.e. a coercion from ty2 to ty1 is already defined;
function ls cannot be used as a coercion, e.g. ty1 = ty2;
a coercion from ty1 to ty2 is already defined

val find : t -> Ttypes.ty -> Ttypes.ty -> Tterm.lsymbol list

returns the coercion, or raises Not_found

val union : t -> t -> t

union s1 s2 merges the coercions from s2 into s1 (as a new set of coercions) this is asymetric: a coercion from s2 may hide a coercion from s1

val print_coercions : Format.formatter -> t -> unit