mcrl2/data/pos.h

Include file:

#include "mcrl2/data/pos.h"

The standard sort pos.

This file was generated from the data sort specification mcrl2/data/build/pos.spec.

Functions

function_symbol const &mcrl2::data::sort_pos::add_with_carry()

Constructor for function symbol @addc.

Returns: Function symbol add_with_carry

application mcrl2::data::sort_pos::add_with_carry(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)

Application of function symbol @addc.

Parameters:

  • arg0 A data expression
  • arg1 A data expression
  • arg2 A data expression

Returns: Application of @addc to a number of arguments

core::identifier_string const &mcrl2::data::sort_pos::add_with_carry_name()

Generate identifier @addc.

Returns: Identifier @addc

const data_expression &mcrl2::data::sort_pos::arg(const data_expression &e)

Function for projecting out argument arg from an application.

Parameters:

  • e A data expression

Pre: arg is defined for e

Returns: The argument of e that corresponds to arg

const data_expression &mcrl2::data::sort_pos::arg1(const data_expression &e)

Function for projecting out argument arg1 from an application.

Parameters:

  • e A data expression

Pre: arg1 is defined for e

Returns: The argument of e that corresponds to arg1

const data_expression &mcrl2::data::sort_pos::arg2(const data_expression &e)

Function for projecting out argument arg2 from an application.

Parameters:

  • e A data expression

Pre: arg2 is defined for e

Returns: The argument of e that corresponds to arg2

const data_expression &mcrl2::data::sort_pos::arg3(const data_expression &e)

Function for projecting out argument arg3 from an application.

Parameters:

  • e A data expression

Pre: arg3 is defined for e

Returns: The argument of e that corresponds to arg3

function_symbol const &mcrl2::data::sort_pos::c1()

Constructor for function symbol @c1.

Returns: Function symbol c1

core::identifier_string const &mcrl2::data::sort_pos::c1_name()

Generate identifier @c1.

Returns: Identifier @c1

function_symbol const &mcrl2::data::sort_pos::cdub()

Constructor for function symbol @cDub.

Returns: Function symbol cdub

application mcrl2::data::sort_pos::cdub(const data_expression &arg0, const data_expression &arg1)

Application of function symbol @cDub.

Parameters:

  • arg0 A data expression
  • arg1 A data expression

Returns: Application of @cDub to a number of arguments

core::identifier_string const &mcrl2::data::sort_pos::cdub_name()

Generate identifier @cDub.

Returns: Identifier @cDub

bool mcrl2::data::sort_pos::is_add_with_carry_application(const atermpp::aterm_appl &e)

Recogniser for application of @addc.

Parameters:

  • e A data expression

Returns: true iff e is an application of function symbol add_with_carry to a number of arguments

bool mcrl2::data::sort_pos::is_add_with_carry_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @addc.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching @addc

bool mcrl2::data::sort_pos::is_c1_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @c1.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching @c1

bool mcrl2::data::sort_pos::is_cdub_application(const atermpp::aterm_appl &e)

Recogniser for application of @cDub.

Parameters:

  • e A data expression

Returns: true iff e is an application of function symbol cdub to a number of arguments

bool mcrl2::data::sort_pos::is_cdub_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @cDub.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching @cDub

bool mcrl2::data::sort_pos::is_maximum_application(const atermpp::aterm_appl &e)

Recogniser for application of max.

Parameters:

  • e A data expression

Returns: true iff e is an application of function symbol maximum to a number of arguments

bool mcrl2::data::sort_pos::is_maximum_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function max.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching max

bool mcrl2::data::sort_pos::is_minimum_application(const atermpp::aterm_appl &e)

Recogniser for application of min.

Parameters:

  • e A data expression

Returns: true iff e is an application of function symbol minimum to a number of arguments

bool mcrl2::data::sort_pos::is_minimum_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function min.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching min

bool mcrl2::data::sort_pos::is_plus_application(const atermpp::aterm_appl &e)

Recogniser for application of +.

Parameters:

  • e A data expression

Returns: true iff e is an application of function symbol plus to a number of arguments

bool mcrl2::data::sort_pos::is_plus_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function +.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching +

bool mcrl2::data::sort_pos::is_pos(const sort_expression &e)

Recogniser for sort expression Pos.

Parameters:

  • e A sort expression

Returns: true iff e == pos()

bool mcrl2::data::sort_pos::is_pos_predecessor_application(const atermpp::aterm_appl &e)

Recogniser for application of @pospred.

Parameters:

  • e A data expression

Returns: true iff e is an application of function symbol pos_predecessor to a number of arguments

bool mcrl2::data::sort_pos::is_pos_predecessor_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @pospred.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching @pospred

bool mcrl2::data::sort_pos::is_powerlog2_pos_application(const atermpp::aterm_appl &e)

Recogniser for application of @powerlog2.

Parameters:

  • e A data expression

Returns: true iff e is an application of function symbol powerlog2_pos to a number of arguments

bool mcrl2::data::sort_pos::is_powerlog2_pos_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @powerlog2.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching @powerlog2

bool mcrl2::data::sort_pos::is_succ_application(const atermpp::aterm_appl &e)

Recogniser for application of succ.

Parameters:

  • e A data expression

Returns: true iff e is an application of function symbol succ to a number of arguments

bool mcrl2::data::sort_pos::is_succ_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function succ.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching succ

bool mcrl2::data::sort_pos::is_times_application(const atermpp::aterm_appl &e)

Recogniser for application of *.

Parameters:

  • e A data expression

Returns: true iff e is an application of function symbol times to a number of arguments

bool mcrl2::data::sort_pos::is_times_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function *.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching *

const data_expression &mcrl2::data::sort_pos::left(const data_expression &e)

Function for projecting out argument left from an application.

Parameters:

  • e A data expression

Pre: left is defined for e

Returns: The argument of e that corresponds to left

function_symbol const &mcrl2::data::sort_pos::maximum()

Constructor for function symbol max.

Returns: Function symbol maximum

application mcrl2::data::sort_pos::maximum(const data_expression &arg0, const data_expression &arg1)

Application of function symbol max.

Parameters:

  • arg0 A data expression
  • arg1 A data expression

Returns: Application of max to a number of arguments

core::identifier_string const &mcrl2::data::sort_pos::maximum_name()

Generate identifier max.

Returns: Identifier max

function_symbol const &mcrl2::data::sort_pos::minimum()

Constructor for function symbol min.

Returns: Function symbol minimum

application mcrl2::data::sort_pos::minimum(const data_expression &arg0, const data_expression &arg1)

Application of function symbol min.

Parameters:

  • arg0 A data expression
  • arg1 A data expression

Returns: Application of min to a number of arguments

core::identifier_string const &mcrl2::data::sort_pos::minimum_name()

Generate identifier min.

Returns: Identifier min

function_symbol const &mcrl2::data::sort_pos::plus()

Constructor for function symbol +.

Returns: Function symbol plus

application mcrl2::data::sort_pos::plus(const data_expression &arg0, const data_expression &arg1)

Application of function symbol +.

Parameters:

  • arg0 A data expression
  • arg1 A data expression

Returns: Application of + to a number of arguments

core::identifier_string const &mcrl2::data::sort_pos::plus_name()

Generate identifier +.

Returns: Identifier +

basic_sort const &mcrl2::data::sort_pos::pos()

Constructor for sort expression Pos.

Returns: Sort expression Pos

function_symbol_vector mcrl2::data::sort_pos::pos_generate_constructors_code()

Give all system defined constructors for pos.

Returns: All system defined constructors for pos

data_equation_vector mcrl2::data::sort_pos::pos_generate_equations_code()

Give all system defined equations for pos.

Returns: All system defined equations for sort pos

function_symbol_vector mcrl2::data::sort_pos::pos_generate_functions_code()

Give all system defined mappings for pos.

Returns: All system defined mappings for pos

core::identifier_string const &mcrl2::data::sort_pos::pos_name()
function_symbol const &mcrl2::data::sort_pos::pos_predecessor()

Constructor for function symbol @pospred.

Returns: Function symbol pos_predecessor

application mcrl2::data::sort_pos::pos_predecessor(const data_expression &arg0)

Application of function symbol @pospred.

Parameters:

  • arg0 A data expression

Returns: Application of @pospred to a number of arguments

core::identifier_string const &mcrl2::data::sort_pos::pos_predecessor_name()

Generate identifier @pospred.

Returns: Identifier @pospred

function_symbol const &mcrl2::data::sort_pos::powerlog2_pos()

Constructor for function symbol @powerlog2.

Returns: Function symbol powerlog2_pos

application mcrl2::data::sort_pos::powerlog2_pos(const data_expression &arg0)

Application of function symbol @powerlog2.

Parameters:

  • arg0 A data expression

Returns: Application of @powerlog2 to a number of arguments

core::identifier_string const &mcrl2::data::sort_pos::powerlog2_pos_name()

Generate identifier @powerlog2.

Returns: Identifier @powerlog2

const data_expression &mcrl2::data::sort_pos::right(const data_expression &e)

Function for projecting out argument right from an application.

Parameters:

  • e A data expression

Pre: right is defined for e

Returns: The argument of e that corresponds to right

function_symbol const &mcrl2::data::sort_pos::succ()

Constructor for function symbol succ.

Returns: Function symbol succ

application mcrl2::data::sort_pos::succ(const data_expression &arg0)

Application of function symbol succ.

Parameters:

  • arg0 A data expression

Returns: Application of succ to a number of arguments

core::identifier_string const &mcrl2::data::sort_pos::succ_name()

Generate identifier succ.

Returns: Identifier succ

function_symbol const &mcrl2::data::sort_pos::times()

Constructor for function symbol *.

Returns: Function symbol times

application mcrl2::data::sort_pos::times(const data_expression &arg0, const data_expression &arg1)

Application of function symbol *.

Parameters:

  • arg0 A data expression
  • arg1 A data expression

Returns: Application of * to a number of arguments

core::identifier_string const &mcrl2::data::sort_pos::times_name()

Generate identifier *.

Returns: Identifier *