mcrl2/data/bag.h

Include file:

#include "mcrl2/data/bag.h"

The standard sort bag.

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

Typedefs

type mcrl2::data::sort_bag::implementation_map

typedef for std::map< function_symbol, std::pair< std::function< data_expression(const data_expression &)>, std::string > >

Functions

function_symbol mcrl2::data::sort_bag::add_function(const sort_expression &s)

Constructor for function symbol @add_.

Parameters:

  • s A sort expression.

Returns: Function symbol add_function.

application mcrl2::data::sort_bag::add_function(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Application of function symbol @add_.

Parameters:

  • s A sort expression.

  • arg0 A data expression.

  • arg1 A data expression.

Returns: Application of @add_ to a number of arguments.

const core::identifier_string &mcrl2::data::sort_bag::add_function_name()

Generate identifier @add_.

Returns: Identifier @add_.

const data_expression &mcrl2::data::sort_bag::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_bag::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_bag::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_bag::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.

const data_expression &mcrl2::data::sort_bag::arg4(const data_expression &e)

Function for projecting out argument. arg4 from an application.

Parameters:

  • e A data expression.

Pre: arg4 is defined for e.

Returns: The argument of e that corresponds to arg4.

container_sort mcrl2::data::sort_bag::bag(const sort_expression &s)

Constructor for sort expression Bag(S)

Parameters:

  • s A sort expression

Returns: Sort expression bag(s)

function_symbol mcrl2::data::sort_bag::bag2set(const sort_expression &s)

Constructor for function symbol Bag2Set.

Parameters:

  • s A sort expression.

Returns: Function symbol bag2set.

application mcrl2::data::sort_bag::bag2set(const sort_expression &s, const data_expression &arg0)

Application of function symbol Bag2Set.

Parameters:

  • s A sort expression.

  • arg0 A data expression.

Returns: Application of Bag2Set to a number of arguments.

const core::identifier_string &mcrl2::data::sort_bag::bag2set_name()

Generate identifier Bag2Set.

Returns: Identifier Bag2Set.

function_symbol mcrl2::data::sort_bag::bag_comprehension(const sort_expression &s)

Constructor for function symbol @bagcomp.

Parameters:

  • s A sort expression.

Returns: Function symbol bag_comprehension.

application mcrl2::data::sort_bag::bag_comprehension(const sort_expression &s, const data_expression &arg0)

Application of function symbol @bagcomp.

Parameters:

  • s A sort expression.

  • arg0 A data expression.

Returns: Application of @bagcomp to a number of arguments.

const core::identifier_string &mcrl2::data::sort_bag::bag_comprehension_name()

Generate identifier @bagcomp.

Returns: Identifier @bagcomp.

implementation_map mcrl2::data::sort_bag::bag_cpp_implementable_constructors(const sort_expression &s)

Give all system defined constructors which have an implementation in C++ and not in rewrite rules for bag.

Parameters:

  • s A sort expression.

Returns: All system defined constructors that are to be implemented in C++ for bag.

implementation_map mcrl2::data::sort_bag::bag_cpp_implementable_mappings(const sort_expression &s)

Give all system defined mappings that are to be implemented in C++ code for bag.

Parameters:

  • s A sort expression

Returns: A mapping from C++ implementable function symbols to system defined mappings implemented in C++ code for bag

function_symbol mcrl2::data::sort_bag::bag_fbag(const sort_expression &s)

Constructor for function symbol @bagfbag.

Parameters:

  • s A sort expression.

Returns: Function symbol bag_fbag.

application mcrl2::data::sort_bag::bag_fbag(const sort_expression &s, const data_expression &arg0)

Application of function symbol @bagfbag.

Parameters:

  • s A sort expression.

  • arg0 A data expression.

Returns: Application of @bagfbag to a number of arguments.

const core::identifier_string &mcrl2::data::sort_bag::bag_fbag_name()

Generate identifier @bagfbag.

Returns: Identifier @bagfbag.

function_symbol_vector mcrl2::data::sort_bag::bag_generate_constructors_and_functions_code(const sort_expression &s)

Give all system defined mappings and constructors for bag.

Parameters:

  • s A sort expression

Returns: All system defined mappings for bag

function_symbol_vector mcrl2::data::sort_bag::bag_generate_constructors_code(const sort_expression &s)

Give all system defined constructors for bag.

Parameters:

  • s A sort expression.

Returns: All system defined constructors for bag.

data_equation_vector mcrl2::data::sort_bag::bag_generate_equations_code(const sort_expression &s)

Give all system defined equations for bag.

Parameters:

  • s A sort expression

Returns: All system defined equations for sort bag

function_symbol_vector mcrl2::data::sort_bag::bag_generate_functions_code(const sort_expression &s)

Give all system defined mappings for bag.

Parameters:

  • s A sort expression

Returns: All system defined mappings for bag

function_symbol_vector mcrl2::data::sort_bag::bag_mCRL2_usable_constructors(const sort_expression &s)

Give all defined constructors which can be used in mCRL2 specs for bag.

Parameters:

  • s A sort expression.

Returns: All system defined constructors that can be used in an mCRL2 specification for bag.

function_symbol_vector mcrl2::data::sort_bag::bag_mCRL2_usable_mappings(const sort_expression &s)

Give all system defined mappings that can be used in mCRL2 specs for bag.

Parameters:

  • s A sort expression

Returns: All system defined mappings for that can be used in mCRL2 specificationis bag

function_symbol mcrl2::data::sort_bag::bool2nat_function(const sort_expression &s)

Constructor for function symbol @Bool2Nat_.

Parameters:

  • s A sort expression.

Returns: Function symbol bool2nat_function.

application mcrl2::data::sort_bag::bool2nat_function(const sort_expression &s, const data_expression &arg0)

Application of function symbol @Bool2Nat_.

Parameters:

  • s A sort expression.

  • arg0 A data expression.

Returns: Application of @Bool2Nat_ to a number of arguments.

const core::identifier_string &mcrl2::data::sort_bag::bool2nat_function_name()

Generate identifier @Bool2Nat_.

Returns: Identifier @Bool2Nat_.

function_symbol mcrl2::data::sort_bag::constructor(const sort_expression &s)

Constructor for function symbol @bag.

Parameters:

  • s A sort expression.

Returns: Function symbol constructor.

application mcrl2::data::sort_bag::constructor(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Application of function symbol @bag.

Parameters:

  • s A sort expression.

  • arg0 A data expression.

  • arg1 A data expression.

Returns: Application of @bag to a number of arguments.

const core::identifier_string &mcrl2::data::sort_bag::constructor_name()

Generate identifier @bag.

Returns: Identifier @bag.

function_symbol mcrl2::data::sort_bag::count(const sort_expression&, const sort_expression &s0, const sort_expression &s1)
application mcrl2::data::sort_bag::count(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Application of function symbol count.

Parameters:

  • s A sort expression.

  • arg0 A data expression.

  • arg1 A data expression.

Returns: Application of count to a number of arguments.

const core::identifier_string &mcrl2::data::sort_bag::count_name()

Generate identifier count.

Returns: Identifier count.

function_symbol mcrl2::data::sort_bag::difference(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
application mcrl2::data::sort_bag::difference(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Application of function symbol -.

Parameters:

  • s A sort expression.

  • arg0 A data expression.

  • arg1 A data expression.

Returns: Application of - to a number of arguments.

const core::identifier_string &mcrl2::data::sort_bag::difference_name()

Generate identifier -.

Returns: Identifier -.

function_symbol mcrl2::data::sort_bag::fbag2fset(const sort_expression &s)

Constructor for function symbol @fbag2fset.

Parameters:

  • s A sort expression.

Returns: Function symbol fbag2fset.

application mcrl2::data::sort_bag::fbag2fset(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Application of function symbol @fbag2fset.

Parameters:

  • s A sort expression.

  • arg0 A data expression.

  • arg1 A data expression.

Returns: Application of @fbag2fset to a number of arguments.

const core::identifier_string &mcrl2::data::sort_bag::fbag2fset_name()

Generate identifier @fbag2fset.

Returns: Identifier @fbag2fset.

function_symbol mcrl2::data::sort_bag::fbag_difference(const sort_expression &s)

Constructor for function symbol @fbag_diff.

Parameters:

  • s A sort expression.

Returns: Function symbol fbag_difference.

application mcrl2::data::sort_bag::fbag_difference(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)

Application of function symbol @fbag_diff.

Parameters:

  • s A sort expression.

  • arg0 A data expression.

  • arg1 A data expression.

  • arg2 A data expression.

  • arg3 A data expression.

Returns: Application of @fbag_diff to a number of arguments.

const core::identifier_string &mcrl2::data::sort_bag::fbag_difference_name()

Generate identifier @fbag_diff.

Returns: Identifier @fbag_diff.

function_symbol mcrl2::data::sort_bag::fbag_intersect(const sort_expression &s)

Constructor for function symbol @fbag_inter.

Parameters:

  • s A sort expression.

Returns: Function symbol fbag_intersect.

application mcrl2::data::sort_bag::fbag_intersect(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)

Application of function symbol @fbag_inter.

Parameters:

  • s A sort expression.

  • arg0 A data expression.

  • arg1 A data expression.

  • arg2 A data expression.

  • arg3 A data expression.

Returns: Application of @fbag_inter to a number of arguments.

const core::identifier_string &mcrl2::data::sort_bag::fbag_intersect_name()

Generate identifier @fbag_inter.

Returns: Identifier @fbag_inter.

function_symbol mcrl2::data::sort_bag::fbag_join(const sort_expression &s)

Constructor for function symbol @fbag_join.

Parameters:

  • s A sort expression.

Returns: Function symbol fbag_join.

application mcrl2::data::sort_bag::fbag_join(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)

Application of function symbol @fbag_join.

Parameters:

  • s A sort expression.

  • arg0 A data expression.

  • arg1 A data expression.

  • arg2 A data expression.

  • arg3 A data expression.

Returns: Application of @fbag_join to a number of arguments.

const core::identifier_string &mcrl2::data::sort_bag::fbag_join_name()

Generate identifier @fbag_join.

Returns: Identifier @fbag_join.

function_symbol mcrl2::data::sort_bag::in(const sort_expression&, const sort_expression &s0, const sort_expression &s1)
application mcrl2::data::sort_bag::in(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Application of function symbol in.

Parameters:

  • s A sort expression.

  • arg0 A data expression.

  • arg1 A data expression.

Returns: Application of in to a number of arguments.

const core::identifier_string &mcrl2::data::sort_bag::in_name()

Generate identifier in.

Returns: Identifier in.

function_symbol mcrl2::data::sort_bag::intersection(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
application mcrl2::data::sort_bag::intersection(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Application of function symbol *.

Parameters:

  • s A sort expression.

  • arg0 A data expression.

  • arg1 A data expression.

Returns: Application of * to a number of arguments.

const core::identifier_string &mcrl2::data::sort_bag::intersection_name()

Generate identifier *.

Returns: Identifier *.

bool mcrl2::data::sort_bag::is_add_function_application(const atermpp::aterm_appl &e)

Recogniser for application of @add_.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_bag::is_add_function_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @add_.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching @add_.

bool mcrl2::data::sort_bag::is_bag(const sort_expression &e)

Recogniser for sort expression Bag(s)

Parameters:

  • e A sort expression

Returns: true iff e is a container sort of which the name matches bag

bool mcrl2::data::sort_bag::is_bag2set_application(const atermpp::aterm_appl &e)

Recogniser for application of Bag2Set.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_bag::is_bag2set_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function Bag2Set.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching Bag2Set.

bool mcrl2::data::sort_bag::is_bag_comprehension_application(const atermpp::aterm_appl &e)

Recogniser for application of @bagcomp.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_bag::is_bag_comprehension_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @bagcomp.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching @bagcomp.

bool mcrl2::data::sort_bag::is_bag_fbag_application(const atermpp::aterm_appl &e)

Recogniser for application of @bagfbag.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_bag::is_bag_fbag_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @bagfbag.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching @bagfbag.

bool mcrl2::data::sort_bag::is_bool2nat_function_application(const atermpp::aterm_appl &e)

Recogniser for application of @Bool2Nat_.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_bag::is_bool2nat_function_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @Bool2Nat_.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching @Bool2Nat_.

bool mcrl2::data::sort_bag::is_constructor_application(const atermpp::aterm_appl &e)

Recogniser for application of @bag.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_bag::is_constructor_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @bag.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching @bag.

bool mcrl2::data::sort_bag::is_count_application(const atermpp::aterm_appl &e)

Recogniser for application of count.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_bag::is_count_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function count.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching count.

bool mcrl2::data::sort_bag::is_difference_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 difference to a number of arguments.

bool mcrl2::data::sort_bag::is_difference_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_bag::is_fbag2fset_application(const atermpp::aterm_appl &e)

Recogniser for application of @fbag2fset.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_bag::is_fbag2fset_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @fbag2fset.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching @fbag2fset.

bool mcrl2::data::sort_bag::is_fbag_difference_application(const atermpp::aterm_appl &e)

Recogniser for application of @fbag_diff.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_bag::is_fbag_difference_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @fbag_diff.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching @fbag_diff.

bool mcrl2::data::sort_bag::is_fbag_intersect_application(const atermpp::aterm_appl &e)

Recogniser for application of @fbag_inter.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_bag::is_fbag_intersect_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @fbag_inter.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching @fbag_inter.

bool mcrl2::data::sort_bag::is_fbag_join_application(const atermpp::aterm_appl &e)

Recogniser for application of @fbag_join.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_bag::is_fbag_join_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @fbag_join.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching @fbag_join.

bool mcrl2::data::sort_bag::is_in_application(const atermpp::aterm_appl &e)

Recogniser for application of in.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_bag::is_in_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function in.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching in.

bool mcrl2::data::sort_bag::is_intersection_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 intersection to a number of arguments.

bool mcrl2::data::sort_bag::is_intersection_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_bag::is_min_function_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 min_function to a number of arguments.

bool mcrl2::data::sort_bag::is_min_function_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_bag::is_monus_function_application(const atermpp::aterm_appl &e)

Recogniser for application of @monus_.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_bag::is_monus_function_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @monus_.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching @monus_.

bool mcrl2::data::sort_bag::is_nat2bool_function_application(const atermpp::aterm_appl &e)

Recogniser for application of @Nat2Bool_.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_bag::is_nat2bool_function_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @Nat2Bool_.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching @Nat2Bool_.

bool mcrl2::data::sort_bag::is_one_function_application(const atermpp::aterm_appl &e)

Recogniser for application of @one_.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_bag::is_one_function_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @one_.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching @one_.

bool mcrl2::data::sort_bag::is_set2bag_application(const atermpp::aterm_appl &e)

Recogniser for application of Set2Bag.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_bag::is_set2bag_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function Set2Bag.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching Set2Bag.

bool mcrl2::data::sort_bag::is_union_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 union_ to a number of arguments.

bool mcrl2::data::sort_bag::is_union_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_bag::is_zero_function_application(const atermpp::aterm_appl &e)

Recogniser for application of @zero_.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_bag::is_zero_function_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @zero_.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching @zero_.

const data_expression &mcrl2::data::sort_bag::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 mcrl2::data::sort_bag::min_function(const sort_expression &s)

Constructor for function symbol @min_.

Parameters:

  • s A sort expression.

Returns: Function symbol min_function.

application mcrl2::data::sort_bag::min_function(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Application of function symbol @min_.

Parameters:

  • s A sort expression.

  • arg0 A data expression.

  • arg1 A data expression.

Returns: Application of @min_ to a number of arguments.

const core::identifier_string &mcrl2::data::sort_bag::min_function_name()

Generate identifier @min_.

Returns: Identifier @min_.

function_symbol mcrl2::data::sort_bag::monus_function(const sort_expression &s)

Constructor for function symbol @monus_.

Parameters:

  • s A sort expression.

Returns: Function symbol monus_function.

application mcrl2::data::sort_bag::monus_function(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Application of function symbol @monus_.

Parameters:

  • s A sort expression.

  • arg0 A data expression.

  • arg1 A data expression.

Returns: Application of @monus_ to a number of arguments.

const core::identifier_string &mcrl2::data::sort_bag::monus_function_name()

Generate identifier @monus_.

Returns: Identifier @monus_.

function_symbol mcrl2::data::sort_bag::nat2bool_function(const sort_expression &s)

Constructor for function symbol @Nat2Bool_.

Parameters:

  • s A sort expression.

Returns: Function symbol nat2bool_function.

application mcrl2::data::sort_bag::nat2bool_function(const sort_expression &s, const data_expression &arg0)

Application of function symbol @Nat2Bool_.

Parameters:

  • s A sort expression.

  • arg0 A data expression.

Returns: Application of @Nat2Bool_ to a number of arguments.

const core::identifier_string &mcrl2::data::sort_bag::nat2bool_function_name()

Generate identifier @Nat2Bool_.

Returns: Identifier @Nat2Bool_.

function_symbol mcrl2::data::sort_bag::one_function(const sort_expression &s)

Constructor for function symbol @one_.

Parameters:

  • s A sort expression.

Returns: Function symbol one_function.

application mcrl2::data::sort_bag::one_function(const sort_expression &s, const data_expression &arg0)

Application of function symbol @one_.

Parameters:

  • s A sort expression.

  • arg0 A data expression.

Returns: Application of @one_ to a number of arguments.

const core::identifier_string &mcrl2::data::sort_bag::one_function_name()

Generate identifier @one_.

Returns: Identifier @one_.

const data_expression &mcrl2::data::sort_bag::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 mcrl2::data::sort_bag::set2bag(const sort_expression &s)

Constructor for function symbol Set2Bag.

Parameters:

  • s A sort expression.

Returns: Function symbol set2bag.

application mcrl2::data::sort_bag::set2bag(const sort_expression &s, const data_expression &arg0)

Application of function symbol Set2Bag.

Parameters:

  • s A sort expression.

  • arg0 A data expression.

Returns: Application of Set2Bag to a number of arguments.

const core::identifier_string &mcrl2::data::sort_bag::set2bag_name()

Generate identifier Set2Bag.

Returns: Identifier Set2Bag.

function_symbol mcrl2::data::sort_bag::union_(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
application mcrl2::data::sort_bag::union_(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Application of function symbol +.

Parameters:

  • s A sort expression.

  • arg0 A data expression.

  • arg1 A data expression.

Returns: Application of + to a number of arguments.

const core::identifier_string &mcrl2::data::sort_bag::union_name()

Generate identifier +.

Returns: Identifier +.

function_symbol mcrl2::data::sort_bag::zero_function(const sort_expression &s)

Constructor for function symbol @zero_.

Parameters:

  • s A sort expression.

Returns: Function symbol zero_function.

application mcrl2::data::sort_bag::zero_function(const sort_expression &s, const data_expression &arg0)

Application of function symbol @zero_.

Parameters:

  • s A sort expression.

  • arg0 A data expression.

Returns: Application of @zero_ to a number of arguments.

const core::identifier_string &mcrl2::data::sort_bag::zero_function_name()

Generate identifier @zero_.

Returns: Identifier @zero_.