package pratter

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Parameter `Make.Sup`

type term

The main type of terms, that contains symbols, applications, binary and unary operators.

type pos

The type of positions.

type popt = pos option

type ident

Type of identifiers of symbols.

val get_ident : term -> (ident * popt) option

get_ident t returns the identifier and (optional) position of term t, if t is an identifier.

val make_appl : term -> term -> term

make_appl t u returns the application of t to u, sometimes noted @(t, u), or just t u.

val make_bin_appl : 
  term ->
  popt ->
  (ident * associativity * priority) ->
  term ->
  term

make_bin_appl t p op u returns the application of binary operator op in position p to terms t and u, so the term t op u.

val make_una_appl : popt -> (ident * priority) -> term -> term

make_una_appl p op t returns the application of unary operator op in position p to term t, so the term op t.