package gospel

You can search for identifiers within the package.

in-package search v0.2.0

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

Legend:
Library
Module
Module type
Parameter
Class
Class type

module Ident = Identifier.Ident

type pattern = {

p_node : pattern_node;
p_ty : Ttypes.ty;
p_loc : Ppxlib.Location.t;

}

and pattern_node =

| Pwild
(*
_
*)
| Pvar of Symbols.vsymbol
(*
x
*)
| Papp of Symbols.lsymbol * pattern list
(*
Constructor
*)
| Por of pattern * pattern
(*
p1 | p2
*)
| Pas of pattern * Symbols.vsymbol
(*
p as vs
*)
| Pinterval of char * char
| Pconst of Ppxlib.constant

val pp_pattern : 
  Ppx_deriving_runtime.Format.formatter ->
  pattern ->
  Ppx_deriving_runtime.unit

val show_pattern : pattern -> Ppx_deriving_runtime.string

val pp_pattern_node : 
  Ppx_deriving_runtime.Format.formatter ->
  pattern_node ->
  Ppx_deriving_runtime.unit

val show_pattern_node : pattern_node -> Ppx_deriving_runtime.string

type binop =

| Tand
| Tand_asym
| Tor
| Tor_asym
| Timplies
| Tiff

val pp_binop : 
  Ppx_deriving_runtime.Format.formatter ->
  binop ->
  Ppx_deriving_runtime.unit

val show_binop : binop -> Ppx_deriving_runtime.string

type quant =

| Tforall
| Texists

val pp_quant : 
  Ppx_deriving_runtime.Format.formatter ->
  quant ->
  Ppx_deriving_runtime.unit

val show_quant : quant -> Ppx_deriving_runtime.string

type term = {

t_node : term_node;
t_ty : Ttypes.ty option;
t_attrs : string list;
t_loc : Ppxlib.Location.t;

}

and term_node =

| Tvar of Symbols.vsymbol
| Tconst of Ppxlib.constant
| Tapp of Symbols.lsymbol * term list
| Tfield of term * Symbols.lsymbol
| Tif of term * term * term
| Tlet of Symbols.vsymbol * term * term
| Tcase of term * (pattern * term option * term) list
| Tquant of quant * Symbols.vsymbol list * term
| Tlambda of pattern list * term
| Tbinop of binop * term * term
| Tnot of term
| Told of term
| Ttrue
| Tfalse

val pp_term : 
  Ppx_deriving_runtime.Format.formatter ->
  term ->
  Ppx_deriving_runtime.unit

val show_term : term -> Ppx_deriving_runtime.string

val pp_term_node : 
  Ppx_deriving_runtime.Format.formatter ->
  term_node ->
  Ppx_deriving_runtime.unit

val show_term_node : term_node -> Ppx_deriving_runtime.string