Struct Eqlog

pub struct Eqlog { /* private fields */ }

A model of the Eqlog theory.

Implementations

impl Eqlog

pub fn new() -> Self

Creates an empty model.

pub fn close(&mut self)

Closes the model under all axioms. Depending on the axioms and the model, this may run indefinitely.

pub fn close_until(&mut self, condition: impl Fn(&Self) -> bool) -> bool

Closes the model under all axioms until condition is satisfied. Depending on the axioms and condition, this may run indefinitely. Returns true if the condition eventually holds. Returns false if the model could be closed under all axioms but condition still does not hold.

pub fn iter_ident(&self) -> impl '_ + Iterator<Item = Ident>

Returns and iterator over elements of sort Ident. The iterator yields canonical representatives only.

pub fn root_ident(&self, el: Ident) -> Ident

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_ident(&self, lhs: Ident, rhs: Ident) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_virt_ident(&self) -> impl '_ + Iterator<Item = VirtIdent>

Returns and iterator over elements of sort VirtIdent. The iterator yields canonical representatives only.

pub fn root_virt_ident(&self, el: VirtIdent) -> VirtIdent

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_virt_ident(&self, lhs: VirtIdent, rhs: VirtIdent) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_type_decl_node(&self) -> impl '_ + Iterator<Item = TypeDeclNode>

Returns and iterator over elements of sort TypeDeclNode. The iterator yields canonical representatives only.

pub fn root_type_decl_node(&self, el: TypeDeclNode) -> TypeDeclNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_type_decl_node( &self, lhs: TypeDeclNode, rhs: TypeDeclNode, ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_arg_decl_node(&self) -> impl '_ + Iterator<Item = ArgDeclNode>

Returns and iterator over elements of sort ArgDeclNode. The iterator yields canonical representatives only.

pub fn root_arg_decl_node(&self, el: ArgDeclNode) -> ArgDeclNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_arg_decl_node( &self, lhs: ArgDeclNode, rhs: ArgDeclNode, ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_arg_decl_list_node( &self, ) -> impl '_ + Iterator<Item = ArgDeclListNode>

Returns and iterator over elements of sort ArgDeclListNode. The iterator yields canonical representatives only.

pub fn root_arg_decl_list_node(&self, el: ArgDeclListNode) -> ArgDeclListNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_arg_decl_list_node( &self, lhs: ArgDeclListNode, rhs: ArgDeclListNode, ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_pred_decl_node(&self) -> impl '_ + Iterator<Item = PredDeclNode>

Returns and iterator over elements of sort PredDeclNode. The iterator yields canonical representatives only.

pub fn root_pred_decl_node(&self, el: PredDeclNode) -> PredDeclNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_pred_decl_node( &self, lhs: PredDeclNode, rhs: PredDeclNode, ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_func_decl_node(&self) -> impl '_ + Iterator<Item = FuncDeclNode>

Returns and iterator over elements of sort FuncDeclNode. The iterator yields canonical representatives only.

pub fn root_func_decl_node(&self, el: FuncDeclNode) -> FuncDeclNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_func_decl_node( &self, lhs: FuncDeclNode, rhs: FuncDeclNode, ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_ctor_decl_node(&self) -> impl '_ + Iterator<Item = CtorDeclNode>

Returns and iterator over elements of sort CtorDeclNode. The iterator yields canonical representatives only.

pub fn root_ctor_decl_node(&self, el: CtorDeclNode) -> CtorDeclNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_ctor_decl_node( &self, lhs: CtorDeclNode, rhs: CtorDeclNode, ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_ctor_decl_list_node( &self, ) -> impl '_ + Iterator<Item = CtorDeclListNode>

Returns and iterator over elements of sort CtorDeclListNode. The iterator yields canonical representatives only.

pub fn root_ctor_decl_list_node(&self, el: CtorDeclListNode) -> CtorDeclListNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_ctor_decl_list_node( &self, lhs: CtorDeclListNode, rhs: CtorDeclListNode, ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_enum_decl_node(&self) -> impl '_ + Iterator<Item = EnumDeclNode>

Returns and iterator over elements of sort EnumDeclNode. The iterator yields canonical representatives only.

pub fn root_enum_decl_node(&self, el: EnumDeclNode) -> EnumDeclNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_enum_decl_node( &self, lhs: EnumDeclNode, rhs: EnumDeclNode, ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_term_node(&self) -> impl '_ + Iterator<Item = TermNode>

Returns and iterator over elements of sort TermNode. The iterator yields canonical representatives only.

pub fn root_term_node(&self, el: TermNode) -> TermNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_term_node(&self, lhs: TermNode, rhs: TermNode) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_term_list_node(&self) -> impl '_ + Iterator<Item = TermListNode>

Returns and iterator over elements of sort TermListNode. The iterator yields canonical representatives only.

pub fn root_term_list_node(&self, el: TermListNode) -> TermListNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_term_list_node( &self, lhs: TermListNode, rhs: TermListNode, ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_opt_term_node(&self) -> impl '_ + Iterator<Item = OptTermNode>

Returns and iterator over elements of sort OptTermNode. The iterator yields canonical representatives only.

pub fn root_opt_term_node(&self, el: OptTermNode) -> OptTermNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_opt_term_node( &self, lhs: OptTermNode, rhs: OptTermNode, ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_match_case_node(&self) -> impl '_ + Iterator<Item = MatchCaseNode>

Returns and iterator over elements of sort MatchCaseNode. The iterator yields canonical representatives only.

pub fn root_match_case_node(&self, el: MatchCaseNode) -> MatchCaseNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_match_case_node( &self, lhs: MatchCaseNode, rhs: MatchCaseNode, ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_stmt_list_node(&self) -> impl '_ + Iterator<Item = StmtListNode>

Returns and iterator over elements of sort StmtListNode. The iterator yields canonical representatives only.

pub fn root_stmt_list_node(&self, el: StmtListNode) -> StmtListNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_stmt_list_node( &self, lhs: StmtListNode, rhs: StmtListNode, ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_match_case_list_node( &self, ) -> impl '_ + Iterator<Item = MatchCaseListNode>

Returns and iterator over elements of sort MatchCaseListNode. The iterator yields canonical representatives only.

pub fn root_match_case_list_node( &self, el: MatchCaseListNode, ) -> MatchCaseListNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_match_case_list_node( &self, lhs: MatchCaseListNode, rhs: MatchCaseListNode, ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_if_atom_node(&self) -> impl '_ + Iterator<Item = IfAtomNode>

Returns and iterator over elements of sort IfAtomNode. The iterator yields canonical representatives only.

pub fn root_if_atom_node(&self, el: IfAtomNode) -> IfAtomNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_if_atom_node(&self, lhs: IfAtomNode, rhs: IfAtomNode) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_then_atom_node(&self) -> impl '_ + Iterator<Item = ThenAtomNode>

Returns and iterator over elements of sort ThenAtomNode. The iterator yields canonical representatives only.

pub fn root_then_atom_node(&self, el: ThenAtomNode) -> ThenAtomNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_then_atom_node( &self, lhs: ThenAtomNode, rhs: ThenAtomNode, ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_stmt_node(&self) -> impl '_ + Iterator<Item = StmtNode>

Returns and iterator over elements of sort StmtNode. The iterator yields canonical representatives only.

pub fn root_stmt_node(&self, el: StmtNode) -> StmtNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_stmt_node(&self, lhs: StmtNode, rhs: StmtNode) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_stmt_block_list_node( &self, ) -> impl '_ + Iterator<Item = StmtBlockListNode>

Returns and iterator over elements of sort StmtBlockListNode. The iterator yields canonical representatives only.

pub fn root_stmt_block_list_node( &self, el: StmtBlockListNode, ) -> StmtBlockListNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_stmt_block_list_node( &self, lhs: StmtBlockListNode, rhs: StmtBlockListNode, ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_rule_decl_node(&self) -> impl '_ + Iterator<Item = RuleDeclNode>

Returns and iterator over elements of sort RuleDeclNode. The iterator yields canonical representatives only.

pub fn root_rule_decl_node(&self, el: RuleDeclNode) -> RuleDeclNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_rule_decl_node( &self, lhs: RuleDeclNode, rhs: RuleDeclNode, ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_decl_node(&self) -> impl '_ + Iterator<Item = DeclNode>

Returns and iterator over elements of sort DeclNode. The iterator yields canonical representatives only.

pub fn root_decl_node(&self, el: DeclNode) -> DeclNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_decl_node(&self, lhs: DeclNode, rhs: DeclNode) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_decl_list_node(&self) -> impl '_ + Iterator<Item = DeclListNode>

Returns and iterator over elements of sort DeclListNode. The iterator yields canonical representatives only.

pub fn root_decl_list_node(&self, el: DeclListNode) -> DeclListNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_decl_list_node( &self, lhs: DeclListNode, rhs: DeclListNode, ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_module_node(&self) -> impl '_ + Iterator<Item = ModuleNode>

Returns and iterator over elements of sort ModuleNode. The iterator yields canonical representatives only.

pub fn root_module_node(&self, el: ModuleNode) -> ModuleNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_module_node(&self, lhs: ModuleNode, rhs: ModuleNode) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_loc(&self) -> impl '_ + Iterator<Item = Loc>

Returns and iterator over elements of sort Loc. The iterator yields canonical representatives only.

pub fn root_loc(&self, el: Loc) -> Loc

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_loc(&self, lhs: Loc, rhs: Loc) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_rule_descendant_node( &self, ) -> impl '_ + Iterator<Item = RuleDescendantNode>

Returns and iterator over elements of sort RuleDescendantNode. The iterator yields canonical representatives only.

pub fn root_rule_descendant_node( &self, el: RuleDescendantNode, ) -> RuleDescendantNode

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_rule_descendant_node( &self, lhs: RuleDescendantNode, rhs: RuleDescendantNode, ) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_scope(&self) -> impl '_ + Iterator<Item = Scope>

Returns and iterator over elements of sort Scope. The iterator yields canonical representatives only.

pub fn root_scope(&self, el: Scope) -> Scope

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_scope(&self, lhs: Scope, rhs: Scope) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_type(&self) -> impl '_ + Iterator<Item = Type>

Returns and iterator over elements of sort Type. The iterator yields canonical representatives only.

pub fn root_type(&self, el: Type) -> Type

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_type(&self, lhs: Type, rhs: Type) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_type_list(&self) -> impl '_ + Iterator<Item = TypeList>

Returns and iterator over elements of sort TypeList. The iterator yields canonical representatives only.

pub fn root_type_list(&self, el: TypeList) -> TypeList

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_type_list(&self, lhs: TypeList, rhs: TypeList) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_pred(&self) -> impl '_ + Iterator<Item = Pred>

Returns and iterator over elements of sort Pred. The iterator yields canonical representatives only.

pub fn root_pred(&self, el: Pred) -> Pred

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_pred(&self, lhs: Pred, rhs: Pred) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_func(&self) -> impl '_ + Iterator<Item = Func>

Returns and iterator over elements of sort Func. The iterator yields canonical representatives only.

pub fn root_func(&self, el: Func) -> Func

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_func(&self, lhs: Func, rhs: Func) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_rel(&self) -> impl '_ + Iterator<Item = Rel>

Returns and iterator over elements of sort Rel. The iterator yields canonical representatives only.

pub fn root_rel(&self, el: Rel) -> Rel

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_rel(&self, lhs: Rel, rhs: Rel) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_structure(&self) -> impl '_ + Iterator<Item = Structure>

Returns and iterator over elements of sort Structure. The iterator yields canonical representatives only.

pub fn root_structure(&self, el: Structure) -> Structure

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_structure(&self, lhs: Structure, rhs: Structure) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_el(&self) -> impl '_ + Iterator<Item = El>

Returns and iterator over elements of sort El. The iterator yields canonical representatives only.

pub fn root_el(&self, el: El) -> El

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_el(&self, lhs: El, rhs: El) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_el_list(&self) -> impl '_ + Iterator<Item = ElList>

Returns and iterator over elements of sort ElList. The iterator yields canonical representatives only.

pub fn root_el_list(&self, el: ElList) -> ElList

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_el_list(&self, lhs: ElList, rhs: ElList) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_el_name(&self) -> impl '_ + Iterator<Item = ElName>

Returns and iterator over elements of sort ElName. The iterator yields canonical representatives only.

pub fn root_el_name(&self, el: ElName) -> ElName

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_el_name(&self, lhs: ElName, rhs: ElName) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_morphism(&self) -> impl '_ + Iterator<Item = Morphism>

Returns and iterator over elements of sort Morphism. The iterator yields canonical representatives only.

pub fn root_morphism(&self, el: Morphism) -> Morphism

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_morphism(&self, lhs: Morphism, rhs: Morphism) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_symbol_kind(&self) -> impl '_ + Iterator<Item = SymbolKind>

Returns and iterator over elements of sort SymbolKind. The iterator yields canonical representatives only.

pub fn root_symbol_kind(&self, el: SymbolKind) -> SymbolKind

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_symbol_kind(&self, lhs: SymbolKind, rhs: SymbolKind) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn iter_nat(&self) -> impl '_ + Iterator<Item = Nat>

Returns and iterator over elements of sort Nat. The iterator yields canonical representatives only.

pub fn root_nat(&self, el: Nat) -> Nat

Returns the canonical representative of the equivalence class of el.

pub fn are_equal_nat(&self, lhs: Nat, rhs: Nat) -> bool

Returns true if lhs and rhs are in the same equivalence class.

pub fn equate_ident(&mut self, lhs: Ident, rhs: Ident)

Enforces the equality lhs = rhs.

pub fn equate_virt_ident(&mut self, lhs: VirtIdent, rhs: VirtIdent)

Enforces the equality lhs = rhs.

pub fn equate_type_decl_node(&mut self, lhs: TypeDeclNode, rhs: TypeDeclNode)

Enforces the equality lhs = rhs.

pub fn equate_arg_decl_node(&mut self, lhs: ArgDeclNode, rhs: ArgDeclNode)

Enforces the equality lhs = rhs.

pub fn equate_arg_decl_list_node( &mut self, lhs: ArgDeclListNode, rhs: ArgDeclListNode, )

Enforces the equality lhs = rhs.

pub fn equate_pred_decl_node(&mut self, lhs: PredDeclNode, rhs: PredDeclNode)

Enforces the equality lhs = rhs.

pub fn equate_func_decl_node(&mut self, lhs: FuncDeclNode, rhs: FuncDeclNode)

Enforces the equality lhs = rhs.

pub fn equate_ctor_decl_node(&mut self, lhs: CtorDeclNode, rhs: CtorDeclNode)

Enforces the equality lhs = rhs.

pub fn equate_ctor_decl_list_node( &mut self, lhs: CtorDeclListNode, rhs: CtorDeclListNode, )

Enforces the equality lhs = rhs.

pub fn equate_enum_decl_node(&mut self, lhs: EnumDeclNode, rhs: EnumDeclNode)

Enforces the equality lhs = rhs.

pub fn equate_term_node(&mut self, lhs: TermNode, rhs: TermNode)

Enforces the equality lhs = rhs.

pub fn equate_term_list_node(&mut self, lhs: TermListNode, rhs: TermListNode)

Enforces the equality lhs = rhs.

pub fn equate_opt_term_node(&mut self, lhs: OptTermNode, rhs: OptTermNode)

Enforces the equality lhs = rhs.

pub fn equate_match_case_node(&mut self, lhs: MatchCaseNode, rhs: MatchCaseNode)

Enforces the equality lhs = rhs.

pub fn equate_match_case_list_node( &mut self, lhs: MatchCaseListNode, rhs: MatchCaseListNode, )

Enforces the equality lhs = rhs.

pub fn equate_if_atom_node(&mut self, lhs: IfAtomNode, rhs: IfAtomNode)

Enforces the equality lhs = rhs.

pub fn equate_then_atom_node(&mut self, lhs: ThenAtomNode, rhs: ThenAtomNode)

Enforces the equality lhs = rhs.

pub fn equate_stmt_node(&mut self, lhs: StmtNode, rhs: StmtNode)

Enforces the equality lhs = rhs.

pub fn equate_stmt_list_node(&mut self, lhs: StmtListNode, rhs: StmtListNode)

Enforces the equality lhs = rhs.

pub fn equate_stmt_block_list_node( &mut self, lhs: StmtBlockListNode, rhs: StmtBlockListNode, )

Enforces the equality lhs = rhs.

pub fn equate_rule_decl_node(&mut self, lhs: RuleDeclNode, rhs: RuleDeclNode)

Enforces the equality lhs = rhs.

pub fn equate_decl_node(&mut self, lhs: DeclNode, rhs: DeclNode)

Enforces the equality lhs = rhs.

pub fn equate_decl_list_node(&mut self, lhs: DeclListNode, rhs: DeclListNode)

Enforces the equality lhs = rhs.

pub fn equate_module_node(&mut self, lhs: ModuleNode, rhs: ModuleNode)

Enforces the equality lhs = rhs.

pub fn equate_loc(&mut self, lhs: Loc, rhs: Loc)

Enforces the equality lhs = rhs.

pub fn equate_rule_descendant_node( &mut self, lhs: RuleDescendantNode, rhs: RuleDescendantNode, )

Enforces the equality lhs = rhs.

pub fn equate_scope(&mut self, lhs: Scope, rhs: Scope)

Enforces the equality lhs = rhs.

pub fn equate_type(&mut self, lhs: Type, rhs: Type)

Enforces the equality lhs = rhs.

pub fn equate_pred(&mut self, lhs: Pred, rhs: Pred)

Enforces the equality lhs = rhs.

pub fn equate_func(&mut self, lhs: Func, rhs: Func)

Enforces the equality lhs = rhs.

pub fn equate_structure(&mut self, lhs: Structure, rhs: Structure)

Enforces the equality lhs = rhs.

pub fn equate_el(&mut self, lhs: El, rhs: El)

Enforces the equality lhs = rhs.

pub fn equate_el_name(&mut self, lhs: ElName, rhs: ElName)

Enforces the equality lhs = rhs.

pub fn equate_morphism(&mut self, lhs: Morphism, rhs: Morphism)

Enforces the equality lhs = rhs.

pub fn equate_symbol_kind(&mut self, lhs: SymbolKind, rhs: SymbolKind)

Enforces the equality lhs = rhs.

pub fn equate_nat(&mut self, lhs: Nat, rhs: Nat)

Enforces the equality lhs = rhs.

pub fn equate_type_list(&mut self, lhs: TypeList, rhs: TypeList)

Enforces the equality lhs = rhs.

pub fn equate_rel(&mut self, lhs: Rel, rhs: Rel)

Enforces the equality lhs = rhs.

pub fn equate_el_list(&mut self, lhs: ElList, rhs: ElList)

Enforces the equality lhs = rhs.

pub fn new_ident(&mut self) -> Ident

Adjoins a new element of type Ident.

pub fn new_virt_ident(&mut self) -> VirtIdent

Adjoins a new element of type VirtIdent.

pub fn new_type_decl_node(&mut self) -> TypeDeclNode

Adjoins a new element of type TypeDeclNode.

pub fn new_arg_decl_node(&mut self) -> ArgDeclNode

Adjoins a new element of type ArgDeclNode.

pub fn new_arg_decl_list_node(&mut self) -> ArgDeclListNode

Adjoins a new element of type ArgDeclListNode.

pub fn new_pred_decl_node(&mut self) -> PredDeclNode

Adjoins a new element of type PredDeclNode.

pub fn new_func_decl_node(&mut self) -> FuncDeclNode

Adjoins a new element of type FuncDeclNode.

pub fn new_ctor_decl_node(&mut self) -> CtorDeclNode

Adjoins a new element of type CtorDeclNode.

pub fn new_ctor_decl_list_node(&mut self) -> CtorDeclListNode

Adjoins a new element of type CtorDeclListNode.

pub fn new_enum_decl_node(&mut self) -> EnumDeclNode

Adjoins a new element of type EnumDeclNode.

pub fn new_term_node(&mut self) -> TermNode

Adjoins a new element of type TermNode.

pub fn new_term_list_node(&mut self) -> TermListNode

Adjoins a new element of type TermListNode.

pub fn new_opt_term_node(&mut self) -> OptTermNode

Adjoins a new element of type OptTermNode.

pub fn new_match_case_node(&mut self) -> MatchCaseNode

Adjoins a new element of type MatchCaseNode.

pub fn new_match_case_list_node(&mut self) -> MatchCaseListNode

Adjoins a new element of type MatchCaseListNode.

pub fn new_if_atom_node(&mut self) -> IfAtomNode

Adjoins a new element of type IfAtomNode.

pub fn new_then_atom_node(&mut self) -> ThenAtomNode

Adjoins a new element of type ThenAtomNode.

pub fn new_stmt_node(&mut self) -> StmtNode

Adjoins a new element of type StmtNode.

pub fn new_stmt_list_node(&mut self) -> StmtListNode

Adjoins a new element of type StmtListNode.

pub fn new_stmt_block_list_node(&mut self) -> StmtBlockListNode

Adjoins a new element of type StmtBlockListNode.

pub fn new_rule_decl_node(&mut self) -> RuleDeclNode

Adjoins a new element of type RuleDeclNode.

pub fn new_decl_node(&mut self) -> DeclNode

Adjoins a new element of type DeclNode.

pub fn new_decl_list_node(&mut self) -> DeclListNode

Adjoins a new element of type DeclListNode.

pub fn new_module_node(&mut self) -> ModuleNode

Adjoins a new element of type ModuleNode.

pub fn new_loc(&mut self) -> Loc

Adjoins a new element of type Loc.

pub fn new_rule_descendant_node(&mut self) -> RuleDescendantNode

Adjoins a new element of type RuleDescendantNode.

pub fn new_scope(&mut self) -> Scope

Adjoins a new element of type Scope.

pub fn new_type(&mut self) -> Type

Adjoins a new element of type Type.

pub fn new_pred(&mut self) -> Pred

Adjoins a new element of type Pred.

pub fn new_func(&mut self) -> Func

Adjoins a new element of type Func.

pub fn new_structure(&mut self) -> Structure

Adjoins a new element of type Structure.

pub fn new_el(&mut self) -> El

Adjoins a new element of type El.

pub fn new_el_name(&mut self) -> ElName

Adjoins a new element of type ElName.

pub fn new_morphism(&mut self) -> Morphism

Adjoins a new element of type Morphism.

pub fn new_symbol_kind(&mut self) -> SymbolKind

Adjoins a new element of type SymbolKind.

pub fn new_nat(&mut self) -> Nat

Adjoins a new element of type Nat.

pub fn new_type_list(&mut self, value: TypeListEnum) -> TypeList

Adjoins a new element of type TypeList.

pub fn new_rel(&mut self, value: RelEnum) -> Rel

Adjoins a new element of type Rel.

pub fn new_el_list(&mut self, value: ElListEnum) -> ElList

Adjoins a new element of type ElList.

pub fn real_virt_ident(&self, arg0: Ident) -> Option<VirtIdent>

Evaluates real_virt_ident(arg0).

pub fn iter_real_virt_ident( &self, ) -> impl '_ + Iterator<Item = (Ident, VirtIdent)>

Returns an iterator over tuples in the graph of the real_virt_ident function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_real_virt_ident(&mut self, tm0: Ident, tm1: VirtIdent)

Makes the equation real_virt_ident(tm0) = tm1 hold.

pub fn virt_real_ident(&self, arg0: VirtIdent) -> Option<Ident>

Evaluates virt_real_ident(arg0).

pub fn iter_virt_real_ident( &self, ) -> impl '_ + Iterator<Item = (VirtIdent, Ident)>

Returns an iterator over tuples in the graph of the virt_real_ident function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_virt_real_ident(&mut self, tm0: VirtIdent, tm1: Ident)

Makes the equation virt_real_ident(tm0) = tm1 hold.

pub fn var(&self, arg0: Structure, arg1: ElName) -> Option<El>

Evaluates var(arg0, arg1).

pub fn iter_var(&self) -> impl '_ + Iterator<Item = (Structure, ElName, El)>

Returns an iterator over tuples in the graph of the var function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_var(&mut self, tm0: Structure, tm1: ElName, tm2: El)

Makes the equation var(tm0, tm1) = tm2 hold.

pub fn rule_name(&self, arg0: RuleDeclNode) -> Option<Ident>

Evaluates rule_name(arg0).

pub fn iter_rule_name(&self) -> impl '_ + Iterator<Item = (RuleDeclNode, Ident)>

Returns an iterator over tuples in the graph of the rule_name function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_rule_name(&mut self, tm0: RuleDeclNode, tm1: Ident)

Makes the equation rule_name(tm0) = tm1 hold.

pub fn type_decl_node_loc(&self, arg0: TypeDeclNode) -> Option<Loc>

Evaluates type_decl_node_loc(arg0).

pub fn iter_type_decl_node_loc( &self, ) -> impl '_ + Iterator<Item = (TypeDeclNode, Loc)>

Returns an iterator over tuples in the graph of the type_decl_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_type_decl_node_loc(&mut self, tm0: TypeDeclNode, tm1: Loc)

Makes the equation type_decl_node_loc(tm0) = tm1 hold.

pub fn arg_decl_node_loc(&self, arg0: ArgDeclNode) -> Option<Loc>

Evaluates arg_decl_node_loc(arg0).

pub fn iter_arg_decl_node_loc( &self, ) -> impl '_ + Iterator<Item = (ArgDeclNode, Loc)>

Returns an iterator over tuples in the graph of the arg_decl_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_arg_decl_node_loc(&mut self, tm0: ArgDeclNode, tm1: Loc)

Makes the equation arg_decl_node_loc(tm0) = tm1 hold.

pub fn arg_decl_list_node_loc(&self, arg0: ArgDeclListNode) -> Option<Loc>

Evaluates arg_decl_list_node_loc(arg0).

pub fn iter_arg_decl_list_node_loc( &self, ) -> impl '_ + Iterator<Item = (ArgDeclListNode, Loc)>

Returns an iterator over tuples in the graph of the arg_decl_list_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_arg_decl_list_node_loc(&mut self, tm0: ArgDeclListNode, tm1: Loc)

Makes the equation arg_decl_list_node_loc(tm0) = tm1 hold.

pub fn pred_decl_node_loc(&self, arg0: PredDeclNode) -> Option<Loc>

Evaluates pred_decl_node_loc(arg0).

pub fn iter_pred_decl_node_loc( &self, ) -> impl '_ + Iterator<Item = (PredDeclNode, Loc)>

Returns an iterator over tuples in the graph of the pred_decl_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_pred_decl_node_loc(&mut self, tm0: PredDeclNode, tm1: Loc)

Makes the equation pred_decl_node_loc(tm0) = tm1 hold.

pub fn func_decl_node_loc(&self, arg0: FuncDeclNode) -> Option<Loc>

Evaluates func_decl_node_loc(arg0).

pub fn iter_func_decl_node_loc( &self, ) -> impl '_ + Iterator<Item = (FuncDeclNode, Loc)>

Returns an iterator over tuples in the graph of the func_decl_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_func_decl_node_loc(&mut self, tm0: FuncDeclNode, tm1: Loc)

Makes the equation func_decl_node_loc(tm0) = tm1 hold.

pub fn ctor_decl_node_loc(&self, arg0: CtorDeclNode) -> Option<Loc>

Evaluates ctor_decl_node_loc(arg0).

pub fn iter_ctor_decl_node_loc( &self, ) -> impl '_ + Iterator<Item = (CtorDeclNode, Loc)>

Returns an iterator over tuples in the graph of the ctor_decl_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_ctor_decl_node_loc(&mut self, tm0: CtorDeclNode, tm1: Loc)

Makes the equation ctor_decl_node_loc(tm0) = tm1 hold.

pub fn enum_decl_node_loc(&self, arg0: EnumDeclNode) -> Option<Loc>

Evaluates enum_decl_node_loc(arg0).

pub fn iter_enum_decl_node_loc( &self, ) -> impl '_ + Iterator<Item = (EnumDeclNode, Loc)>

Returns an iterator over tuples in the graph of the enum_decl_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_enum_decl_node_loc(&mut self, tm0: EnumDeclNode, tm1: Loc)

Makes the equation enum_decl_node_loc(tm0) = tm1 hold.

pub fn term_node_loc(&self, arg0: TermNode) -> Option<Loc>

Evaluates term_node_loc(arg0).

pub fn iter_term_node_loc(&self) -> impl '_ + Iterator<Item = (TermNode, Loc)>

Returns an iterator over tuples in the graph of the term_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_term_node_loc(&mut self, tm0: TermNode, tm1: Loc)

Makes the equation term_node_loc(tm0) = tm1 hold.

pub fn term_list_node_loc(&self, arg0: TermListNode) -> Option<Loc>

Evaluates term_list_node_loc(arg0).

pub fn iter_term_list_node_loc( &self, ) -> impl '_ + Iterator<Item = (TermListNode, Loc)>

Returns an iterator over tuples in the graph of the term_list_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_term_list_node_loc(&mut self, tm0: TermListNode, tm1: Loc)

Makes the equation term_list_node_loc(tm0) = tm1 hold.

pub fn match_case_node_loc(&self, arg0: MatchCaseNode) -> Option<Loc>

Evaluates match_case_node_loc(arg0).

pub fn iter_match_case_node_loc( &self, ) -> impl '_ + Iterator<Item = (MatchCaseNode, Loc)>

Returns an iterator over tuples in the graph of the match_case_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_match_case_node_loc(&mut self, tm0: MatchCaseNode, tm1: Loc)

Makes the equation match_case_node_loc(tm0) = tm1 hold.

pub fn opt_term_node_loc(&self, arg0: OptTermNode) -> Option<Loc>

Evaluates opt_term_node_loc(arg0).

pub fn iter_opt_term_node_loc( &self, ) -> impl '_ + Iterator<Item = (OptTermNode, Loc)>

Returns an iterator over tuples in the graph of the opt_term_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_opt_term_node_loc(&mut self, tm0: OptTermNode, tm1: Loc)

Makes the equation opt_term_node_loc(tm0) = tm1 hold.

pub fn if_atom_node_loc(&self, arg0: IfAtomNode) -> Option<Loc>

Evaluates if_atom_node_loc(arg0).

pub fn iter_if_atom_node_loc( &self, ) -> impl '_ + Iterator<Item = (IfAtomNode, Loc)>

Returns an iterator over tuples in the graph of the if_atom_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_if_atom_node_loc(&mut self, tm0: IfAtomNode, tm1: Loc)

Makes the equation if_atom_node_loc(tm0) = tm1 hold.

pub fn then_atom_node_loc(&self, arg0: ThenAtomNode) -> Option<Loc>

Evaluates then_atom_node_loc(arg0).

pub fn iter_then_atom_node_loc( &self, ) -> impl '_ + Iterator<Item = (ThenAtomNode, Loc)>

Returns an iterator over tuples in the graph of the then_atom_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_then_atom_node_loc(&mut self, tm0: ThenAtomNode, tm1: Loc)

Makes the equation then_atom_node_loc(tm0) = tm1 hold.

pub fn stmt_node_loc(&self, arg0: StmtNode) -> Option<Loc>

Evaluates stmt_node_loc(arg0).

pub fn iter_stmt_node_loc(&self) -> impl '_ + Iterator<Item = (StmtNode, Loc)>

Returns an iterator over tuples in the graph of the stmt_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_stmt_node_loc(&mut self, tm0: StmtNode, tm1: Loc)

Makes the equation stmt_node_loc(tm0) = tm1 hold.

pub fn stmt_list_node_loc(&self, arg0: StmtListNode) -> Option<Loc>

Evaluates stmt_list_node_loc(arg0).

pub fn iter_stmt_list_node_loc( &self, ) -> impl '_ + Iterator<Item = (StmtListNode, Loc)>

Returns an iterator over tuples in the graph of the stmt_list_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_stmt_list_node_loc(&mut self, tm0: StmtListNode, tm1: Loc)

Makes the equation stmt_list_node_loc(tm0) = tm1 hold.

pub fn rule_decl_node_loc(&self, arg0: RuleDeclNode) -> Option<Loc>

Evaluates rule_decl_node_loc(arg0).

pub fn iter_rule_decl_node_loc( &self, ) -> impl '_ + Iterator<Item = (RuleDeclNode, Loc)>

Returns an iterator over tuples in the graph of the rule_decl_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_rule_decl_node_loc(&mut self, tm0: RuleDeclNode, tm1: Loc)

Makes the equation rule_decl_node_loc(tm0) = tm1 hold.

pub fn decl_node_loc(&self, arg0: DeclNode) -> Option<Loc>

Evaluates decl_node_loc(arg0).

pub fn iter_decl_node_loc(&self) -> impl '_ + Iterator<Item = (DeclNode, Loc)>

Returns an iterator over tuples in the graph of the decl_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_decl_node_loc(&mut self, tm0: DeclNode, tm1: Loc)

Makes the equation decl_node_loc(tm0) = tm1 hold.

pub fn decl_list_node_loc(&self, arg0: DeclListNode) -> Option<Loc>

Evaluates decl_list_node_loc(arg0).

pub fn iter_decl_list_node_loc( &self, ) -> impl '_ + Iterator<Item = (DeclListNode, Loc)>

Returns an iterator over tuples in the graph of the decl_list_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_decl_list_node_loc(&mut self, tm0: DeclListNode, tm1: Loc)

Makes the equation decl_list_node_loc(tm0) = tm1 hold.

pub fn module_node_loc(&self, arg0: ModuleNode) -> Option<Loc>

Evaluates module_node_loc(arg0).

pub fn iter_module_node_loc( &self, ) -> impl '_ + Iterator<Item = (ModuleNode, Loc)>

Returns an iterator over tuples in the graph of the module_node_loc function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_module_node_loc(&mut self, tm0: ModuleNode, tm1: Loc)

Makes the equation module_node_loc(tm0) = tm1 hold.

pub fn rule_descendant_rule( &self, arg0: RuleDeclNode, ) -> Option<RuleDescendantNode>

Evaluates rule_descendant_rule(arg0).

pub fn iter_rule_descendant_rule( &self, ) -> impl '_ + Iterator<Item = (RuleDeclNode, RuleDescendantNode)>

Returns an iterator over tuples in the graph of the rule_descendant_rule function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_rule_descendant_rule( &mut self, tm0: RuleDeclNode, tm1: RuleDescendantNode, )

Makes the equation rule_descendant_rule(tm0) = tm1 hold.

pub fn rule_descendant_term(&self, arg0: TermNode) -> Option<RuleDescendantNode>

Evaluates rule_descendant_term(arg0).

pub fn iter_rule_descendant_term( &self, ) -> impl '_ + Iterator<Item = (TermNode, RuleDescendantNode)>

Returns an iterator over tuples in the graph of the rule_descendant_term function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_rule_descendant_term( &mut self, tm0: TermNode, tm1: RuleDescendantNode, )

Makes the equation rule_descendant_term(tm0) = tm1 hold.

pub fn rule_descendant_term_list( &self, arg0: TermListNode, ) -> Option<RuleDescendantNode>

Evaluates rule_descendant_term_list(arg0).

pub fn iter_rule_descendant_term_list( &self, ) -> impl '_ + Iterator<Item = (TermListNode, RuleDescendantNode)>

Returns an iterator over tuples in the graph of the rule_descendant_term_list function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_rule_descendant_term_list( &mut self, tm0: TermListNode, tm1: RuleDescendantNode, )

Makes the equation rule_descendant_term_list(tm0) = tm1 hold.

pub fn rule_descendant_opt_term( &self, arg0: OptTermNode, ) -> Option<RuleDescendantNode>

Evaluates rule_descendant_opt_term(arg0).

pub fn iter_rule_descendant_opt_term( &self, ) -> impl '_ + Iterator<Item = (OptTermNode, RuleDescendantNode)>

Returns an iterator over tuples in the graph of the rule_descendant_opt_term function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_rule_descendant_opt_term( &mut self, tm0: OptTermNode, tm1: RuleDescendantNode, )

Makes the equation rule_descendant_opt_term(tm0) = tm1 hold.

pub fn rule_descendant_if_atom( &self, arg0: IfAtomNode, ) -> Option<RuleDescendantNode>

Evaluates rule_descendant_if_atom(arg0).

pub fn iter_rule_descendant_if_atom( &self, ) -> impl '_ + Iterator<Item = (IfAtomNode, RuleDescendantNode)>

Returns an iterator over tuples in the graph of the rule_descendant_if_atom function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_rule_descendant_if_atom( &mut self, tm0: IfAtomNode, tm1: RuleDescendantNode, )

Makes the equation rule_descendant_if_atom(tm0) = tm1 hold.

pub fn rule_descendant_then_atom( &self, arg0: ThenAtomNode, ) -> Option<RuleDescendantNode>

Evaluates rule_descendant_then_atom(arg0).

pub fn iter_rule_descendant_then_atom( &self, ) -> impl '_ + Iterator<Item = (ThenAtomNode, RuleDescendantNode)>

Returns an iterator over tuples in the graph of the rule_descendant_then_atom function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_rule_descendant_then_atom( &mut self, tm0: ThenAtomNode, tm1: RuleDescendantNode, )

Makes the equation rule_descendant_then_atom(tm0) = tm1 hold.

pub fn rule_descendant_match_case( &self, arg0: MatchCaseNode, ) -> Option<RuleDescendantNode>

Evaluates rule_descendant_match_case(arg0).

pub fn iter_rule_descendant_match_case( &self, ) -> impl '_ + Iterator<Item = (MatchCaseNode, RuleDescendantNode)>

Returns an iterator over tuples in the graph of the rule_descendant_match_case function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_rule_descendant_match_case( &mut self, tm0: MatchCaseNode, tm1: RuleDescendantNode, )

Makes the equation rule_descendant_match_case(tm0) = tm1 hold.

pub fn rule_descendant_match_case_list( &self, arg0: MatchCaseListNode, ) -> Option<RuleDescendantNode>

Evaluates rule_descendant_match_case_list(arg0).

pub fn iter_rule_descendant_match_case_list( &self, ) -> impl '_ + Iterator<Item = (MatchCaseListNode, RuleDescendantNode)>

Returns an iterator over tuples in the graph of the rule_descendant_match_case_list function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_rule_descendant_match_case_list( &mut self, tm0: MatchCaseListNode, tm1: RuleDescendantNode, )

Makes the equation rule_descendant_match_case_list(tm0) = tm1 hold.

pub fn rule_descendant_stmt(&self, arg0: StmtNode) -> Option<RuleDescendantNode>

Evaluates rule_descendant_stmt(arg0).

pub fn iter_rule_descendant_stmt( &self, ) -> impl '_ + Iterator<Item = (StmtNode, RuleDescendantNode)>

Returns an iterator over tuples in the graph of the rule_descendant_stmt function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_rule_descendant_stmt( &mut self, tm0: StmtNode, tm1: RuleDescendantNode, )

Makes the equation rule_descendant_stmt(tm0) = tm1 hold.

pub fn rule_descendant_stmt_list( &self, arg0: StmtListNode, ) -> Option<RuleDescendantNode>

Evaluates rule_descendant_stmt_list(arg0).

pub fn iter_rule_descendant_stmt_list( &self, ) -> impl '_ + Iterator<Item = (StmtListNode, RuleDescendantNode)>

Returns an iterator over tuples in the graph of the rule_descendant_stmt_list function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_rule_descendant_stmt_list( &mut self, tm0: StmtListNode, tm1: RuleDescendantNode, )

Makes the equation rule_descendant_stmt_list(tm0) = tm1 hold.

pub fn rule_descendant_stmt_block_list( &self, arg0: StmtBlockListNode, ) -> Option<RuleDescendantNode>

Evaluates rule_descendant_stmt_block_list(arg0).

pub fn iter_rule_descendant_stmt_block_list( &self, ) -> impl '_ + Iterator<Item = (StmtBlockListNode, RuleDescendantNode)>

Returns an iterator over tuples in the graph of the rule_descendant_stmt_block_list function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_rule_descendant_stmt_block_list( &mut self, tm0: StmtBlockListNode, tm1: RuleDescendantNode, )

Makes the equation rule_descendant_stmt_block_list(tm0) = tm1 hold.

pub fn entry_scope(&self, arg0: RuleDescendantNode) -> Option<Scope>

Evaluates entry_scope(arg0).

pub fn iter_entry_scope( &self, ) -> impl '_ + Iterator<Item = (RuleDescendantNode, Scope)>

Returns an iterator over tuples in the graph of the entry_scope function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_entry_scope(&mut self, tm0: RuleDescendantNode, tm1: Scope)

Makes the equation entry_scope(tm0) = tm1 hold.

pub fn exit_scope(&self, arg0: RuleDescendantNode) -> Option<Scope>

Evaluates exit_scope(arg0).

pub fn iter_exit_scope( &self, ) -> impl '_ + Iterator<Item = (RuleDescendantNode, Scope)>

Returns an iterator over tuples in the graph of the exit_scope function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_exit_scope(&mut self, tm0: RuleDescendantNode, tm1: Scope)

Makes the equation exit_scope(tm0) = tm1 hold.

pub fn ctor_enum(&self, arg0: CtorDeclNode) -> Option<EnumDeclNode>

Evaluates ctor_enum(arg0).

pub fn iter_ctor_enum( &self, ) -> impl '_ + Iterator<Item = (CtorDeclNode, EnumDeclNode)>

Returns an iterator over tuples in the graph of the ctor_enum function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_ctor_enum(&mut self, tm0: CtorDeclNode, tm1: EnumDeclNode)

Makes the equation ctor_enum(tm0) = tm1 hold.

pub fn ctors_enum(&self, arg0: CtorDeclListNode) -> Option<EnumDeclNode>

Evaluates ctors_enum(arg0).

pub fn iter_ctors_enum( &self, ) -> impl '_ + Iterator<Item = (CtorDeclListNode, EnumDeclNode)>

Returns an iterator over tuples in the graph of the ctors_enum function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_ctors_enum(&mut self, tm0: CtorDeclListNode, tm1: EnumDeclNode)

Makes the equation ctors_enum(tm0) = tm1 hold.

pub fn cases_discriminee(&self, arg0: MatchCaseListNode) -> Option<TermNode>

Evaluates cases_discriminee(arg0).

pub fn iter_cases_discriminee( &self, ) -> impl '_ + Iterator<Item = (MatchCaseListNode, TermNode)>

Returns an iterator over tuples in the graph of the cases_discriminee function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_cases_discriminee( &mut self, tm0: MatchCaseListNode, tm1: TermNode, )

Makes the equation cases_discriminee(tm0) = tm1 hold.

pub fn case_discriminee(&self, arg0: MatchCaseNode) -> Option<TermNode>

Evaluates case_discriminee(arg0).

pub fn iter_case_discriminee( &self, ) -> impl '_ + Iterator<Item = (MatchCaseNode, TermNode)>

Returns an iterator over tuples in the graph of the case_discriminee function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_case_discriminee(&mut self, tm0: MatchCaseNode, tm1: TermNode)

Makes the equation case_discriminee(tm0) = tm1 hold.

pub fn desugared_case_equality_atom( &self, arg0: MatchCaseNode, ) -> Option<IfAtomNode>

Evaluates desugared_case_equality_atom(arg0).

pub fn iter_desugared_case_equality_atom( &self, ) -> impl '_ + Iterator<Item = (MatchCaseNode, IfAtomNode)>

Returns an iterator over tuples in the graph of the desugared_case_equality_atom function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_desugared_case_equality_atom( &mut self, tm0: MatchCaseNode, tm1: IfAtomNode, )

Makes the equation desugared_case_equality_atom(tm0) = tm1 hold.

pub fn desugared_case_equality_stmt( &self, arg0: MatchCaseNode, ) -> Option<StmtNode>

Evaluates desugared_case_equality_stmt(arg0).

pub fn iter_desugared_case_equality_stmt( &self, ) -> impl '_ + Iterator<Item = (MatchCaseNode, StmtNode)>

Returns an iterator over tuples in the graph of the desugared_case_equality_stmt function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_desugared_case_equality_stmt( &mut self, tm0: MatchCaseNode, tm1: StmtNode, )

Makes the equation desugared_case_equality_stmt(tm0) = tm1 hold.

pub fn desugared_case_block(&self, arg0: MatchCaseNode) -> Option<StmtListNode>

Evaluates desugared_case_block(arg0).

pub fn iter_desugared_case_block( &self, ) -> impl '_ + Iterator<Item = (MatchCaseNode, StmtListNode)>

Returns an iterator over tuples in the graph of the desugared_case_block function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_desugared_case_block( &mut self, tm0: MatchCaseNode, tm1: StmtListNode, )

Makes the equation desugared_case_block(tm0) = tm1 hold.

pub fn desugared_case_block_list( &self, arg0: MatchCaseListNode, ) -> Option<StmtBlockListNode>

Evaluates desugared_case_block_list(arg0).

pub fn iter_desugared_case_block_list( &self, ) -> impl '_ + Iterator<Item = (MatchCaseListNode, StmtBlockListNode)>

Returns an iterator over tuples in the graph of the desugared_case_block_list function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_desugared_case_block_list( &mut self, tm0: MatchCaseListNode, tm1: StmtBlockListNode, )

Makes the equation desugared_case_block_list(tm0) = tm1 hold.

pub fn nil_type_list(&self) -> Option<TypeList>

Evaluates NilTypeList().

pub fn iter_nil_type_list(&self) -> impl '_ + Iterator<Item = TypeList>

Returns an iterator over NilTypeList constants. The iterator may yield more than one element if the model is not closed.

pub fn insert_nil_type_list(&mut self, tm0: TypeList)

Makes the equation nil_type_list() = tm0 hold.

pub fn cons_type_list(&self, arg0: Type, arg1: TypeList) -> Option<TypeList>

Evaluates ConsTypeList(arg0, arg1).

pub fn iter_cons_type_list( &self, ) -> impl '_ + Iterator<Item = (Type, TypeList, TypeList)>

Returns an iterator over tuples in the graph of the ConsTypeList function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_cons_type_list(&mut self, tm0: Type, tm1: TypeList, tm2: TypeList)

Makes the equation cons_type_list(tm0, tm1) = tm2 hold.

pub fn snoc_type_list(&self, arg0: TypeList, arg1: Type) -> Option<TypeList>

Evaluates SnocTypeList(arg0, arg1).

pub fn iter_snoc_type_list( &self, ) -> impl '_ + Iterator<Item = (TypeList, Type, TypeList)>

Returns an iterator over tuples in the graph of the SnocTypeList function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_snoc_type_list(&mut self, tm0: TypeList, tm1: Type, tm2: TypeList)

Makes the equation snoc_type_list(tm0, tm1) = tm2 hold.

pub fn semantic_type(&self, arg0: Ident) -> Option<Type>

Evaluates semantic_type(arg0).

pub fn iter_semantic_type(&self) -> impl '_ + Iterator<Item = (Ident, Type)>

Returns an iterator over tuples in the graph of the semantic_type function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_semantic_type(&mut self, tm0: Ident, tm1: Type)

Makes the equation semantic_type(tm0) = tm1 hold.

pub fn semantic_arg_types(&self, arg0: ArgDeclListNode) -> Option<TypeList>

Evaluates semantic_arg_types(arg0).

pub fn iter_semantic_arg_types( &self, ) -> impl '_ + Iterator<Item = (ArgDeclListNode, TypeList)>

Returns an iterator over tuples in the graph of the semantic_arg_types function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_semantic_arg_types(&mut self, tm0: ArgDeclListNode, tm1: TypeList)

Makes the equation semantic_arg_types(tm0) = tm1 hold.

pub fn semantic_pred(&self, arg0: Ident) -> Option<Pred>

Evaluates semantic_pred(arg0).

pub fn iter_semantic_pred(&self) -> impl '_ + Iterator<Item = (Ident, Pred)>

Returns an iterator over tuples in the graph of the semantic_pred function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_semantic_pred(&mut self, tm0: Ident, tm1: Pred)

Makes the equation semantic_pred(tm0) = tm1 hold.

pub fn pred_arity(&self, arg0: Pred) -> Option<TypeList>

Evaluates pred_arity(arg0).

pub fn iter_pred_arity(&self) -> impl '_ + Iterator<Item = (Pred, TypeList)>

Returns an iterator over tuples in the graph of the pred_arity function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_pred_arity(&mut self, tm0: Pred, tm1: TypeList)

Makes the equation pred_arity(tm0) = tm1 hold.

pub fn semantic_func(&self, arg0: Ident) -> Option<Func>

Evaluates semantic_func(arg0).

pub fn iter_semantic_func(&self) -> impl '_ + Iterator<Item = (Ident, Func)>

Returns an iterator over tuples in the graph of the semantic_func function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_semantic_func(&mut self, tm0: Ident, tm1: Func)

Makes the equation semantic_func(tm0) = tm1 hold.

pub fn domain(&self, arg0: Func) -> Option<TypeList>

Evaluates domain(arg0).

pub fn iter_domain(&self) -> impl '_ + Iterator<Item = (Func, TypeList)>

Returns an iterator over tuples in the graph of the domain function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_domain(&mut self, tm0: Func, tm1: TypeList)

Makes the equation domain(tm0) = tm1 hold.

pub fn codomain(&self, arg0: Func) -> Option<Type>

Evaluates codomain(arg0).

pub fn iter_codomain(&self) -> impl '_ + Iterator<Item = (Func, Type)>

Returns an iterator over tuples in the graph of the codomain function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_codomain(&mut self, tm0: Func, tm1: Type)

Makes the equation codomain(tm0) = tm1 hold.

pub fn pred_rel(&self, arg0: Pred) -> Option<Rel>

Evaluates PredRel(arg0).

pub fn iter_pred_rel(&self) -> impl '_ + Iterator<Item = (Pred, Rel)>

Returns an iterator over tuples in the graph of the PredRel function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_pred_rel(&mut self, tm0: Pred, tm1: Rel)

Makes the equation pred_rel(tm0) = tm1 hold.

pub fn func_rel(&self, arg0: Func) -> Option<Rel>

Evaluates FuncRel(arg0).

pub fn iter_func_rel(&self) -> impl '_ + Iterator<Item = (Func, Rel)>

Returns an iterator over tuples in the graph of the FuncRel function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_func_rel(&mut self, tm0: Func, tm1: Rel)

Makes the equation func_rel(tm0) = tm1 hold.

pub fn arity(&self, arg0: Rel) -> Option<TypeList>

Evaluates arity(arg0).

pub fn iter_arity(&self) -> impl '_ + Iterator<Item = (Rel, TypeList)>

Returns an iterator over tuples in the graph of the arity function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_arity(&mut self, tm0: Rel, tm1: TypeList)

Makes the equation arity(tm0) = tm1 hold.

pub fn dom(&self, arg0: Morphism) -> Option<Structure>

Evaluates dom(arg0).

pub fn iter_dom(&self) -> impl '_ + Iterator<Item = (Morphism, Structure)>

Returns an iterator over tuples in the graph of the dom function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_dom(&mut self, tm0: Morphism, tm1: Structure)

Makes the equation dom(tm0) = tm1 hold.

pub fn cod(&self, arg0: Morphism) -> Option<Structure>

Evaluates cod(arg0).

pub fn iter_cod(&self) -> impl '_ + Iterator<Item = (Morphism, Structure)>

Returns an iterator over tuples in the graph of the cod function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_cod(&mut self, tm0: Morphism, tm1: Structure)

Makes the equation cod(tm0) = tm1 hold.

pub fn nil_el_list(&self, arg0: Structure) -> Option<ElList>

Evaluates NilElList(arg0).

pub fn iter_nil_el_list(&self) -> impl '_ + Iterator<Item = (Structure, ElList)>

Returns an iterator over tuples in the graph of the NilElList function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_nil_el_list(&mut self, tm0: Structure, tm1: ElList)

Makes the equation nil_el_list(tm0) = tm1 hold.

pub fn cons_el_list(&self, arg0: El, arg1: ElList) -> Option<ElList>

Evaluates ConsElList(arg0, arg1).

pub fn iter_cons_el_list( &self, ) -> impl '_ + Iterator<Item = (El, ElList, ElList)>

Returns an iterator over tuples in the graph of the ConsElList function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_cons_el_list(&mut self, tm0: El, tm1: ElList, tm2: ElList)

Makes the equation cons_el_list(tm0, tm1) = tm2 hold.

pub fn snoc_el_list(&self, arg0: ElList, arg1: El) -> Option<ElList>

Evaluates SnocElList(arg0, arg1).

pub fn iter_snoc_el_list( &self, ) -> impl '_ + Iterator<Item = (ElList, El, ElList)>

Returns an iterator over tuples in the graph of the SnocElList function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_snoc_el_list(&mut self, tm0: ElList, tm1: El, tm2: ElList)

Makes the equation snoc_el_list(tm0, tm1) = tm2 hold.

pub fn el_structure(&self, arg0: El) -> Option<Structure>

Evaluates el_structure(arg0).

pub fn iter_el_structure(&self) -> impl '_ + Iterator<Item = (El, Structure)>

Returns an iterator over tuples in the graph of the el_structure function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_el_structure(&mut self, tm0: El, tm1: Structure)

Makes the equation el_structure(tm0) = tm1 hold.

pub fn els_structure(&self, arg0: ElList) -> Option<Structure>

Evaluates els_structure(arg0).

pub fn iter_els_structure( &self, ) -> impl '_ + Iterator<Item = (ElList, Structure)>

Returns an iterator over tuples in the graph of the els_structure function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_els_structure(&mut self, tm0: ElList, tm1: Structure)

Makes the equation els_structure(tm0) = tm1 hold.

pub fn func_app(&self, arg0: Func, arg1: ElList) -> Option<El>

Evaluates func_app(arg0, arg1).

pub fn iter_func_app(&self) -> impl '_ + Iterator<Item = (Func, ElList, El)>

Returns an iterator over tuples in the graph of the func_app function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_func_app(&mut self, tm0: Func, tm1: ElList, tm2: El)

Makes the equation func_app(tm0, tm1) = tm2 hold.

pub fn map_el(&self, arg0: Morphism, arg1: El) -> Option<El>

Evaluates map_el(arg0, arg1).

pub fn iter_map_el(&self) -> impl '_ + Iterator<Item = (Morphism, El, El)>

Returns an iterator over tuples in the graph of the map_el function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_map_el(&mut self, tm0: Morphism, tm1: El, tm2: El)

Makes the equation map_el(tm0, tm1) = tm2 hold.

pub fn map_els(&self, arg0: Morphism, arg1: ElList) -> Option<ElList>

Evaluates map_els(arg0, arg1).

pub fn iter_map_els( &self, ) -> impl '_ + Iterator<Item = (Morphism, ElList, ElList)>

Returns an iterator over tuples in the graph of the map_els function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_map_els(&mut self, tm0: Morphism, tm1: ElList, tm2: ElList)

Makes the equation map_els(tm0, tm1) = tm2 hold.

pub fn type_symbol(&self) -> Option<SymbolKind>

Evaluates type_symbol().

pub fn iter_type_symbol(&self) -> impl '_ + Iterator<Item = SymbolKind>

Returns an iterator over type_symbol constants. The iterator may yield more than one element if the model is not closed.

pub fn insert_type_symbol(&mut self, tm0: SymbolKind)

Makes the equation type_symbol() = tm0 hold.

pub fn pred_symbol(&self) -> Option<SymbolKind>

Evaluates pred_symbol().

pub fn iter_pred_symbol(&self) -> impl '_ + Iterator<Item = SymbolKind>

Returns an iterator over pred_symbol constants. The iterator may yield more than one element if the model is not closed.

pub fn insert_pred_symbol(&mut self, tm0: SymbolKind)

Makes the equation pred_symbol() = tm0 hold.

pub fn func_symbol(&self) -> Option<SymbolKind>

Evaluates func_symbol().

pub fn iter_func_symbol(&self) -> impl '_ + Iterator<Item = SymbolKind>

Returns an iterator over func_symbol constants. The iterator may yield more than one element if the model is not closed.

pub fn insert_func_symbol(&mut self, tm0: SymbolKind)

Makes the equation func_symbol() = tm0 hold.

pub fn rule_symbol(&self) -> Option<SymbolKind>

Evaluates rule_symbol().

pub fn iter_rule_symbol(&self) -> impl '_ + Iterator<Item = SymbolKind>

Returns an iterator over rule_symbol constants. The iterator may yield more than one element if the model is not closed.

pub fn insert_rule_symbol(&mut self, tm0: SymbolKind)

Makes the equation rule_symbol() = tm0 hold.

pub fn enum_symbol(&self) -> Option<SymbolKind>

Evaluates enum_symbol().

pub fn iter_enum_symbol(&self) -> impl '_ + Iterator<Item = SymbolKind>

Returns an iterator over enum_symbol constants. The iterator may yield more than one element if the model is not closed.

pub fn insert_enum_symbol(&mut self, tm0: SymbolKind)

Makes the equation enum_symbol() = tm0 hold.

pub fn ctor_symbol(&self) -> Option<SymbolKind>

Evaluates ctor_symbol().

pub fn iter_ctor_symbol(&self) -> impl '_ + Iterator<Item = SymbolKind>

Returns an iterator over ctor_symbol constants. The iterator may yield more than one element if the model is not closed.

pub fn insert_ctor_symbol(&mut self, tm0: SymbolKind)

Makes the equation ctor_symbol() = tm0 hold.

pub fn zero(&self) -> Option<Nat>

Evaluates zero().

pub fn iter_zero(&self) -> impl '_ + Iterator<Item = Nat>

Returns an iterator over zero constants. The iterator may yield more than one element if the model is not closed.

pub fn insert_zero(&mut self, tm0: Nat)

Makes the equation zero() = tm0 hold.

pub fn succ(&self, arg0: Nat) -> Option<Nat>

Evaluates succ(arg0).

pub fn iter_succ(&self) -> impl '_ + Iterator<Item = (Nat, Nat)>

Returns an iterator over tuples in the graph of the succ function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_succ(&mut self, tm0: Nat, tm1: Nat)

Makes the equation succ(tm0) = tm1 hold.

pub fn type_list_len(&self, arg0: TypeList) -> Option<Nat>

Evaluates type_list_len(arg0).

pub fn iter_type_list_len(&self) -> impl '_ + Iterator<Item = (TypeList, Nat)>

Returns an iterator over tuples in the graph of the type_list_len function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_type_list_len(&mut self, tm0: TypeList, tm1: Nat)

Makes the equation type_list_len(tm0) = tm1 hold.

pub fn term_list_len(&self, arg0: TermListNode) -> Option<Nat>

Evaluates term_list_len(arg0).

pub fn iter_term_list_len( &self, ) -> impl '_ + Iterator<Item = (TermListNode, Nat)>

Returns an iterator over tuples in the graph of the term_list_len function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_term_list_len(&mut self, tm0: TermListNode, tm1: Nat)

Makes the equation term_list_len(tm0) = tm1 hold.

pub fn before_rule_structure(&self, arg0: RuleDeclNode) -> Option<Structure>

Evaluates before_rule_structure(arg0).

pub fn iter_before_rule_structure( &self, ) -> impl '_ + Iterator<Item = (RuleDeclNode, Structure)>

Returns an iterator over tuples in the graph of the before_rule_structure function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_before_rule_structure( &mut self, tm0: RuleDeclNode, tm1: Structure, )

Makes the equation before_rule_structure(tm0) = tm1 hold.

pub fn if_atom_morphism( &self, arg0: IfAtomNode, arg1: Structure, ) -> Option<Morphism>

Evaluates if_atom_morphism(arg0, arg1).

pub fn iter_if_atom_morphism( &self, ) -> impl '_ + Iterator<Item = (IfAtomNode, Structure, Morphism)>

Returns an iterator over tuples in the graph of the if_atom_morphism function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_if_atom_morphism( &mut self, tm0: IfAtomNode, tm1: Structure, tm2: Morphism, )

Makes the equation if_atom_morphism(tm0, tm1) = tm2 hold.

pub fn then_atom_morphism( &self, arg0: ThenAtomNode, arg1: Structure, ) -> Option<Morphism>

Evaluates then_atom_morphism(arg0, arg1).

pub fn iter_then_atom_morphism( &self, ) -> impl '_ + Iterator<Item = (ThenAtomNode, Structure, Morphism)>

Returns an iterator over tuples in the graph of the then_atom_morphism function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_then_atom_morphism( &mut self, tm0: ThenAtomNode, tm1: Structure, tm2: Morphism, )

Makes the equation then_atom_morphism(tm0, tm1) = tm2 hold.

pub fn branch_stmt_morphism( &self, arg0: StmtNode, arg1: Structure, ) -> Option<Morphism>

Evaluates branch_stmt_morphism(arg0, arg1).

pub fn iter_branch_stmt_morphism( &self, ) -> impl '_ + Iterator<Item = (StmtNode, Structure, Morphism)>

Returns an iterator over tuples in the graph of the branch_stmt_morphism function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_branch_stmt_morphism( &mut self, tm0: StmtNode, tm1: Structure, tm2: Morphism, )

Makes the equation branch_stmt_morphism(tm0, tm1) = tm2 hold.

pub fn match_stmt_morphism( &self, arg0: StmtNode, arg1: Structure, ) -> Option<Morphism>

Evaluates match_stmt_morphism(arg0, arg1).

pub fn iter_match_stmt_morphism( &self, ) -> impl '_ + Iterator<Item = (StmtNode, Structure, Morphism)>

Returns an iterator over tuples in the graph of the match_stmt_morphism function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_match_stmt_morphism( &mut self, tm0: StmtNode, tm1: Structure, tm2: Morphism, )

Makes the equation match_stmt_morphism(tm0, tm1) = tm2 hold.

pub fn semantic_name(&self, arg0: VirtIdent, arg1: Scope) -> Option<ElName>

Evaluates semantic_name(arg0, arg1).

pub fn iter_semantic_name( &self, ) -> impl '_ + Iterator<Item = (VirtIdent, Scope, ElName)>

Returns an iterator over tuples in the graph of the semantic_name function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_semantic_name(&mut self, tm0: VirtIdent, tm1: Scope, tm2: ElName)

Makes the equation semantic_name(tm0, tm1) = tm2 hold.

pub fn semantic_el(&self, arg0: TermNode, arg1: Structure) -> Option<El>

Evaluates semantic_el(arg0, arg1).

pub fn iter_semantic_el( &self, ) -> impl '_ + Iterator<Item = (TermNode, Structure, El)>

Returns an iterator over tuples in the graph of the semantic_el function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_semantic_el(&mut self, tm0: TermNode, tm1: Structure, tm2: El)

Makes the equation semantic_el(tm0, tm1) = tm2 hold.

pub fn semantic_els( &self, arg0: TermListNode, arg1: Structure, ) -> Option<ElList>

Evaluates semantic_els(arg0, arg1).

pub fn iter_semantic_els( &self, ) -> impl '_ + Iterator<Item = (TermListNode, Structure, ElList)>

Returns an iterator over tuples in the graph of the semantic_els function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_semantic_els( &mut self, tm0: TermListNode, tm1: Structure, tm2: ElList, )

Makes the equation semantic_els(tm0, tm1) = tm2 hold.

pub fn wildcard_name(&self, arg0: TermNode) -> Option<ElName>

Evaluates wildcard_name(arg0).

pub fn iter_wildcard_name( &self, ) -> impl '_ + Iterator<Item = (TermNode, ElName)>

Returns an iterator over tuples in the graph of the wildcard_name function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_wildcard_name(&mut self, tm0: TermNode, tm1: ElName)

Makes the equation wildcard_name(tm0) = tm1 hold.

pub fn match_case_pattern_ctor( &self, arg0: MatchCaseNode, ) -> Option<CtorDeclNode>

Evaluates match_case_pattern_ctor(arg0).

pub fn iter_match_case_pattern_ctor( &self, ) -> impl '_ + Iterator<Item = (MatchCaseNode, CtorDeclNode)>

Returns an iterator over tuples in the graph of the match_case_pattern_ctor function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_match_case_pattern_ctor( &mut self, tm0: MatchCaseNode, tm1: CtorDeclNode, )

Makes the equation match_case_pattern_ctor(tm0) = tm1 hold.

pub fn cases_determined_enum( &self, arg0: MatchCaseListNode, ) -> Option<EnumDeclNode>

Evaluates cases_determined_enum(arg0).

pub fn iter_cases_determined_enum( &self, ) -> impl '_ + Iterator<Item = (MatchCaseListNode, EnumDeclNode)>

Returns an iterator over tuples in the graph of the cases_determined_enum function. The relation yielded by the iterator need not be functional if the model is not closed.

pub fn insert_cases_determined_enum( &mut self, tm0: MatchCaseListNode, tm1: EnumDeclNode, )

Makes the equation cases_determined_enum(tm0) = tm1 hold.

pub fn define_real_virt_ident(&mut self, tm0: Ident) -> VirtIdent

Enforces that real_virt_ident(tm0) is defined, adjoining a new element if necessary.

pub fn define_virt_real_ident(&mut self, tm0: VirtIdent) -> Ident

Enforces that virt_real_ident(tm0) is defined, adjoining a new element if necessary.

pub fn define_rule_name(&mut self, tm0: RuleDeclNode) -> Ident

Enforces that rule_name(tm0) is defined, adjoining a new element if necessary.

pub fn define_type_decl_node_loc(&mut self, tm0: TypeDeclNode) -> Loc

Enforces that type_decl_node_loc(tm0) is defined, adjoining a new element if necessary.

pub fn define_arg_decl_node_loc(&mut self, tm0: ArgDeclNode) -> Loc

Enforces that arg_decl_node_loc(tm0) is defined, adjoining a new element if necessary.

pub fn define_arg_decl_list_node_loc(&mut self, tm0: ArgDeclListNode) -> Loc

Enforces that arg_decl_list_node_loc(tm0) is defined, adjoining a new element if necessary.

pub fn define_pred_decl_node_loc(&mut self, tm0: PredDeclNode) -> Loc

Enforces that pred_decl_node_loc(tm0) is defined, adjoining a new element if necessary.

pub fn define_func_decl_node_loc(&mut self, tm0: FuncDeclNode) -> Loc

Enforces that func_decl_node_loc(tm0) is defined, adjoining a new element if necessary.

pub fn define_ctor_decl_node_loc(&mut self, tm0: CtorDeclNode) -> Loc

Enforces that ctor_decl_node_loc(tm0) is defined, adjoining a new element if necessary.

pub fn define_enum_decl_node_loc(&mut self, tm0: EnumDeclNode) -> Loc

Enforces that enum_decl_node_loc(tm0) is defined, adjoining a new element if necessary.

pub fn define_term_node_loc(&mut self, tm0: TermNode) -> Loc

Enforces that term_node_loc(tm0) is defined, adjoining a new element if necessary.

pub fn define_term_list_node_loc(&mut self, tm0: TermListNode) -> Loc

Enforces that term_list_node_loc(tm0) is defined, adjoining a new element if necessary.

pub fn define_match_case_node_loc(&mut self, tm0: MatchCaseNode) -> Loc

Enforces that match_case_node_loc(tm0) is defined, adjoining a new element if necessary.

pub fn define_opt_term_node_loc(&mut self, tm0: OptTermNode) -> Loc

Enforces that opt_term_node_loc(tm0) is defined, adjoining a new element if necessary.

pub fn define_if_atom_node_loc(&mut self, tm0: IfAtomNode) -> Loc

Enforces that if_atom_node_loc(tm0) is defined, adjoining a new element if necessary.

pub fn define_then_atom_node_loc(&mut self, tm0: ThenAtomNode) -> Loc

Enforces that then_atom_node_loc(tm0) is defined, adjoining a new element if necessary.

pub fn define_stmt_node_loc(&mut self, tm0: StmtNode) -> Loc

Enforces that stmt_node_loc(tm0) is defined, adjoining a new element if necessary.

pub fn define_stmt_list_node_loc(&mut self, tm0: StmtListNode) -> Loc

Enforces that stmt_list_node_loc(tm0) is defined, adjoining a new element if necessary.

pub fn define_rule_decl_node_loc(&mut self, tm0: RuleDeclNode) -> Loc

Enforces that rule_decl_node_loc(tm0) is defined, adjoining a new element if necessary.

pub fn define_decl_node_loc(&mut self, tm0: DeclNode) -> Loc

Enforces that decl_node_loc(tm0) is defined, adjoining a new element if necessary.

pub fn define_decl_list_node_loc(&mut self, tm0: DeclListNode) -> Loc

Enforces that decl_list_node_loc(tm0) is defined, adjoining a new element if necessary.

pub fn define_module_node_loc(&mut self, tm0: ModuleNode) -> Loc

Enforces that module_node_loc(tm0) is defined, adjoining a new element if necessary.

pub fn define_rule_descendant_rule( &mut self, tm0: RuleDeclNode, ) -> RuleDescendantNode

Enforces that rule_descendant_rule(tm0) is defined, adjoining a new element if necessary.

pub fn define_rule_descendant_term( &mut self, tm0: TermNode, ) -> RuleDescendantNode

Enforces that rule_descendant_term(tm0) is defined, adjoining a new element if necessary.

pub fn define_rule_descendant_term_list( &mut self, tm0: TermListNode, ) -> RuleDescendantNode

Enforces that rule_descendant_term_list(tm0) is defined, adjoining a new element if necessary.

pub fn define_rule_descendant_opt_term( &mut self, tm0: OptTermNode, ) -> RuleDescendantNode

Enforces that rule_descendant_opt_term(tm0) is defined, adjoining a new element if necessary.

pub fn define_rule_descendant_if_atom( &mut self, tm0: IfAtomNode, ) -> RuleDescendantNode

Enforces that rule_descendant_if_atom(tm0) is defined, adjoining a new element if necessary.

pub fn define_rule_descendant_then_atom( &mut self, tm0: ThenAtomNode, ) -> RuleDescendantNode

Enforces that rule_descendant_then_atom(tm0) is defined, adjoining a new element if necessary.

pub fn define_rule_descendant_match_case( &mut self, tm0: MatchCaseNode, ) -> RuleDescendantNode

Enforces that rule_descendant_match_case(tm0) is defined, adjoining a new element if necessary.

pub fn define_rule_descendant_match_case_list( &mut self, tm0: MatchCaseListNode, ) -> RuleDescendantNode

Enforces that rule_descendant_match_case_list(tm0) is defined, adjoining a new element if necessary.

pub fn define_rule_descendant_stmt( &mut self, tm0: StmtNode, ) -> RuleDescendantNode

Enforces that rule_descendant_stmt(tm0) is defined, adjoining a new element if necessary.

pub fn define_rule_descendant_stmt_list( &mut self, tm0: StmtListNode, ) -> RuleDescendantNode

Enforces that rule_descendant_stmt_list(tm0) is defined, adjoining a new element if necessary.

pub fn define_rule_descendant_stmt_block_list( &mut self, tm0: StmtBlockListNode, ) -> RuleDescendantNode

Enforces that rule_descendant_stmt_block_list(tm0) is defined, adjoining a new element if necessary.

pub fn define_entry_scope(&mut self, tm0: RuleDescendantNode) -> Scope

Enforces that entry_scope(tm0) is defined, adjoining a new element if necessary.

pub fn define_exit_scope(&mut self, tm0: RuleDescendantNode) -> Scope

Enforces that exit_scope(tm0) is defined, adjoining a new element if necessary.

pub fn define_ctor_enum(&mut self, tm0: CtorDeclNode) -> EnumDeclNode

Enforces that ctor_enum(tm0) is defined, adjoining a new element if necessary.

pub fn define_ctors_enum(&mut self, tm0: CtorDeclListNode) -> EnumDeclNode

Enforces that ctors_enum(tm0) is defined, adjoining a new element if necessary.

pub fn define_cases_discriminee(&mut self, tm0: MatchCaseListNode) -> TermNode

Enforces that cases_discriminee(tm0) is defined, adjoining a new element if necessary.

pub fn define_case_discriminee(&mut self, tm0: MatchCaseNode) -> TermNode

Enforces that case_discriminee(tm0) is defined, adjoining a new element if necessary.

pub fn define_desugared_case_equality_atom( &mut self, tm0: MatchCaseNode, ) -> IfAtomNode

Enforces that desugared_case_equality_atom(tm0) is defined, adjoining a new element if necessary.

pub fn define_desugared_case_equality_stmt( &mut self, tm0: MatchCaseNode, ) -> StmtNode

Enforces that desugared_case_equality_stmt(tm0) is defined, adjoining a new element if necessary.

pub fn define_desugared_case_block( &mut self, tm0: MatchCaseNode, ) -> StmtListNode

Enforces that desugared_case_block(tm0) is defined, adjoining a new element if necessary.

pub fn define_desugared_case_block_list( &mut self, tm0: MatchCaseListNode, ) -> StmtBlockListNode

Enforces that desugared_case_block_list(tm0) is defined, adjoining a new element if necessary.

pub fn define_semantic_type(&mut self, tm0: Ident) -> Type

Enforces that semantic_type(tm0) is defined, adjoining a new element if necessary.

pub fn define_semantic_pred(&mut self, tm0: Ident) -> Pred

Enforces that semantic_pred(tm0) is defined, adjoining a new element if necessary.

pub fn define_semantic_func(&mut self, tm0: Ident) -> Func

Enforces that semantic_func(tm0) is defined, adjoining a new element if necessary.

pub fn define_codomain(&mut self, tm0: Func) -> Type

Enforces that codomain(tm0) is defined, adjoining a new element if necessary.

pub fn define_var(&mut self, tm0: Structure, tm1: ElName) -> El

Enforces that var(tm0, tm1) is defined, adjoining a new element if necessary.

pub fn define_el_structure(&mut self, tm0: El) -> Structure

Enforces that el_structure(tm0) is defined, adjoining a new element if necessary.

pub fn define_els_structure(&mut self, tm0: ElList) -> Structure

Enforces that els_structure(tm0) is defined, adjoining a new element if necessary.

pub fn define_func_app(&mut self, tm0: Func, tm1: ElList) -> El

Enforces that func_app(tm0, tm1) is defined, adjoining a new element if necessary.

pub fn define_dom(&mut self, tm0: Morphism) -> Structure

Enforces that dom(tm0) is defined, adjoining a new element if necessary.

pub fn define_cod(&mut self, tm0: Morphism) -> Structure

Enforces that cod(tm0) is defined, adjoining a new element if necessary.

pub fn define_map_el(&mut self, tm0: Morphism, tm1: El) -> El

Enforces that map_el(tm0, tm1) is defined, adjoining a new element if necessary.

pub fn define_type_symbol(&mut self) -> SymbolKind

Enforces that type_symbol() is defined, adjoining a new element if necessary.

pub fn define_pred_symbol(&mut self) -> SymbolKind

Enforces that pred_symbol() is defined, adjoining a new element if necessary.

pub fn define_func_symbol(&mut self) -> SymbolKind

Enforces that func_symbol() is defined, adjoining a new element if necessary.

pub fn define_rule_symbol(&mut self) -> SymbolKind

Enforces that rule_symbol() is defined, adjoining a new element if necessary.

pub fn define_enum_symbol(&mut self) -> SymbolKind

Enforces that enum_symbol() is defined, adjoining a new element if necessary.

pub fn define_ctor_symbol(&mut self) -> SymbolKind

Enforces that ctor_symbol() is defined, adjoining a new element if necessary.

pub fn define_zero(&mut self) -> Nat

Enforces that zero() is defined, adjoining a new element if necessary.

pub fn define_succ(&mut self, tm0: Nat) -> Nat

Enforces that succ(tm0) is defined, adjoining a new element if necessary.

pub fn define_type_list_len(&mut self, tm0: TypeList) -> Nat

Enforces that type_list_len(tm0) is defined, adjoining a new element if necessary.

pub fn define_term_list_len(&mut self, tm0: TermListNode) -> Nat

Enforces that term_list_len(tm0) is defined, adjoining a new element if necessary.

pub fn define_before_rule_structure(&mut self, tm0: RuleDeclNode) -> Structure

Enforces that before_rule_structure(tm0) is defined, adjoining a new element if necessary.

pub fn define_if_atom_morphism( &mut self, tm0: IfAtomNode, tm1: Structure, ) -> Morphism

Enforces that if_atom_morphism(tm0, tm1) is defined, adjoining a new element if necessary.

pub fn define_then_atom_morphism( &mut self, tm0: ThenAtomNode, tm1: Structure, ) -> Morphism

Enforces that then_atom_morphism(tm0, tm1) is defined, adjoining a new element if necessary.

pub fn define_branch_stmt_morphism( &mut self, tm0: StmtNode, tm1: Structure, ) -> Morphism

Enforces that branch_stmt_morphism(tm0, tm1) is defined, adjoining a new element if necessary.

pub fn define_match_stmt_morphism( &mut self, tm0: StmtNode, tm1: Structure, ) -> Morphism

Enforces that match_stmt_morphism(tm0, tm1) is defined, adjoining a new element if necessary.

pub fn define_semantic_name(&mut self, tm0: VirtIdent, tm1: Scope) -> ElName

Enforces that semantic_name(tm0, tm1) is defined, adjoining a new element if necessary.

pub fn define_semantic_el(&mut self, tm0: TermNode, tm1: Structure) -> El

Enforces that semantic_el(tm0, tm1) is defined, adjoining a new element if necessary.

pub fn define_wildcard_name(&mut self, tm0: TermNode) -> ElName

Enforces that wildcard_name(tm0) is defined, adjoining a new element if necessary.

pub fn define_match_case_pattern_ctor( &mut self, tm0: MatchCaseNode, ) -> CtorDeclNode

Enforces that match_case_pattern_ctor(tm0) is defined, adjoining a new element if necessary.

pub fn define_cases_determined_enum( &mut self, tm0: MatchCaseListNode, ) -> EnumDeclNode

Enforces that cases_determined_enum(tm0) is defined, adjoining a new element if necessary.

pub fn define_nil_type_list(&mut self) -> TypeList

Enforces that nil_type_list() is defined, adjoining a new element if necessary.

pub fn define_cons_type_list(&mut self, tm0: Type, tm1: TypeList) -> TypeList

Enforces that cons_type_list(tm0, tm1) is defined, adjoining a new element if necessary.

pub fn define_snoc_type_list(&mut self, tm0: TypeList, tm1: Type) -> TypeList

Enforces that snoc_type_list(tm0, tm1) is defined, adjoining a new element if necessary.

pub fn define_pred_rel(&mut self, tm0: Pred) -> Rel

Enforces that pred_rel(tm0) is defined, adjoining a new element if necessary.

pub fn define_func_rel(&mut self, tm0: Func) -> Rel

Enforces that func_rel(tm0) is defined, adjoining a new element if necessary.

pub fn define_nil_el_list(&mut self, tm0: Structure) -> ElList

Enforces that nil_el_list(tm0) is defined, adjoining a new element if necessary.

pub fn define_cons_el_list(&mut self, tm0: El, tm1: ElList) -> ElList

Enforces that cons_el_list(tm0, tm1) is defined, adjoining a new element if necessary.

pub fn define_snoc_el_list(&mut self, tm0: ElList, tm1: El) -> ElList

Enforces that snoc_el_list(tm0, tm1) is defined, adjoining a new element if necessary.

pub fn absurd(&self) -> bool

Returns true if absurd() holds.

pub fn insert_absurd(&mut self)

Makes absurd() hold.

pub fn type_decl(&self, arg0: TypeDeclNode, arg1: Ident) -> bool

Returns true if type_decl(arg0, arg1) holds.

pub fn iter_type_decl(&self) -> impl '_ + Iterator<Item = (TypeDeclNode, Ident)>

Returns an iterator over tuples of elements satisfying the type_decl predicate.

pub fn insert_type_decl(&mut self, tm0: TypeDeclNode, tm1: Ident)

Makes type_decl(tm0, tm1) hold.

pub fn arg_decl_node_name(&self, arg0: ArgDeclNode, arg1: Ident) -> bool

Returns true if arg_decl_node_name(arg0, arg1) holds.

pub fn iter_arg_decl_node_name( &self, ) -> impl '_ + Iterator<Item = (ArgDeclNode, Ident)>

Returns an iterator over tuples of elements satisfying the arg_decl_node_name predicate.

pub fn insert_arg_decl_node_name(&mut self, tm0: ArgDeclNode, tm1: Ident)

Makes arg_decl_node_name(tm0, tm1) hold.

pub fn arg_decl_node_type(&self, arg0: ArgDeclNode, arg1: Ident) -> bool

Returns true if arg_decl_node_type(arg0, arg1) holds.

pub fn iter_arg_decl_node_type( &self, ) -> impl '_ + Iterator<Item = (ArgDeclNode, Ident)>

Returns an iterator over tuples of elements satisfying the arg_decl_node_type predicate.

pub fn insert_arg_decl_node_type(&mut self, tm0: ArgDeclNode, tm1: Ident)

Makes arg_decl_node_type(tm0, tm1) hold.

pub fn nil_arg_decl_list_node(&self, arg0: ArgDeclListNode) -> bool

Returns true if nil_arg_decl_list_node(arg0) holds.

pub fn iter_nil_arg_decl_list_node( &self, ) -> impl '_ + Iterator<Item = ArgDeclListNode>

Returns an iterator over elements satisfying the nil_arg_decl_list_node predicate.

pub fn insert_nil_arg_decl_list_node(&mut self, tm0: ArgDeclListNode)

Makes nil_arg_decl_list_node(tm0) hold.

pub fn cons_arg_decl_list_node( &self, arg0: ArgDeclListNode, arg1: ArgDeclNode, arg2: ArgDeclListNode, ) -> bool

Returns true if cons_arg_decl_list_node(arg0, arg1, arg2) holds.

pub fn iter_cons_arg_decl_list_node( &self, ) -> impl '_ + Iterator<Item = (ArgDeclListNode, ArgDeclNode, ArgDeclListNode)>

Returns an iterator over tuples of elements satisfying the cons_arg_decl_list_node predicate.

pub fn insert_cons_arg_decl_list_node( &mut self, tm0: ArgDeclListNode, tm1: ArgDeclNode, tm2: ArgDeclListNode, )

Makes cons_arg_decl_list_node(tm0, tm1, tm2) hold.

pub fn pred_decl( &self, arg0: PredDeclNode, arg1: Ident, arg2: ArgDeclListNode, ) -> bool

Returns true if pred_decl(arg0, arg1, arg2) holds.

pub fn iter_pred_decl( &self, ) -> impl '_ + Iterator<Item = (PredDeclNode, Ident, ArgDeclListNode)>

Returns an iterator over tuples of elements satisfying the pred_decl predicate.

pub fn insert_pred_decl( &mut self, tm0: PredDeclNode, tm1: Ident, tm2: ArgDeclListNode, )

Makes pred_decl(tm0, tm1, tm2) hold.

pub fn func_decl( &self, arg0: FuncDeclNode, arg1: Ident, arg2: ArgDeclListNode, arg3: Ident, ) -> bool

Returns true if func_decl(arg0, arg1, arg2, arg3) holds.

pub fn iter_func_decl( &self, ) -> impl '_ + Iterator<Item = (FuncDeclNode, Ident, ArgDeclListNode, Ident)>

Returns an iterator over tuples of elements satisfying the func_decl predicate.

pub fn insert_func_decl( &mut self, tm0: FuncDeclNode, tm1: Ident, tm2: ArgDeclListNode, tm3: Ident, )

Makes func_decl(tm0, tm1, tm2, tm3) hold.

pub fn ctor_decl( &self, arg0: CtorDeclNode, arg1: Ident, arg2: ArgDeclListNode, ) -> bool

Returns true if ctor_decl(arg0, arg1, arg2) holds.

pub fn iter_ctor_decl( &self, ) -> impl '_ + Iterator<Item = (CtorDeclNode, Ident, ArgDeclListNode)>

Returns an iterator over tuples of elements satisfying the ctor_decl predicate.

pub fn insert_ctor_decl( &mut self, tm0: CtorDeclNode, tm1: Ident, tm2: ArgDeclListNode, )

Makes ctor_decl(tm0, tm1, tm2) hold.

pub fn nil_ctor_decl_list_node(&self, arg0: CtorDeclListNode) -> bool

Returns true if nil_ctor_decl_list_node(arg0) holds.

pub fn iter_nil_ctor_decl_list_node( &self, ) -> impl '_ + Iterator<Item = CtorDeclListNode>

Returns an iterator over elements satisfying the nil_ctor_decl_list_node predicate.

pub fn insert_nil_ctor_decl_list_node(&mut self, tm0: CtorDeclListNode)

Makes nil_ctor_decl_list_node(tm0) hold.

pub fn cons_ctor_decl_list_node( &self, arg0: CtorDeclListNode, arg1: CtorDeclNode, arg2: CtorDeclListNode, ) -> bool

Returns true if cons_ctor_decl_list_node(arg0, arg1, arg2) holds.

pub fn iter_cons_ctor_decl_list_node( &self, ) -> impl '_ + Iterator<Item = (CtorDeclListNode, CtorDeclNode, CtorDeclListNode)>

Returns an iterator over tuples of elements satisfying the cons_ctor_decl_list_node predicate.

pub fn insert_cons_ctor_decl_list_node( &mut self, tm0: CtorDeclListNode, tm1: CtorDeclNode, tm2: CtorDeclListNode, )

Makes cons_ctor_decl_list_node(tm0, tm1, tm2) hold.

pub fn enum_decl( &self, arg0: EnumDeclNode, arg1: Ident, arg2: CtorDeclListNode, ) -> bool

Returns true if enum_decl(arg0, arg1, arg2) holds.

pub fn iter_enum_decl( &self, ) -> impl '_ + Iterator<Item = (EnumDeclNode, Ident, CtorDeclListNode)>

Returns an iterator over tuples of elements satisfying the enum_decl predicate.

pub fn insert_enum_decl( &mut self, tm0: EnumDeclNode, tm1: Ident, tm2: CtorDeclListNode, )

Makes enum_decl(tm0, tm1, tm2) hold.

pub fn nil_term_list_node(&self, arg0: TermListNode) -> bool

Returns true if nil_term_list_node(arg0) holds.

pub fn iter_nil_term_list_node(&self) -> impl '_ + Iterator<Item = TermListNode>

Returns an iterator over elements satisfying the nil_term_list_node predicate.

pub fn insert_nil_term_list_node(&mut self, tm0: TermListNode)

Makes nil_term_list_node(tm0) hold.

pub fn cons_term_list_node( &self, arg0: TermListNode, arg1: TermNode, arg2: TermListNode, ) -> bool

Returns true if cons_term_list_node(arg0, arg1, arg2) holds.

pub fn iter_cons_term_list_node( &self, ) -> impl '_ + Iterator<Item = (TermListNode, TermNode, TermListNode)>

Returns an iterator over tuples of elements satisfying the cons_term_list_node predicate.

pub fn insert_cons_term_list_node( &mut self, tm0: TermListNode, tm1: TermNode, tm2: TermListNode, )

Makes cons_term_list_node(tm0, tm1, tm2) hold.

pub fn none_term_node(&self, arg0: OptTermNode) -> bool

Returns true if none_term_node(arg0) holds.

pub fn iter_none_term_node(&self) -> impl '_ + Iterator<Item = OptTermNode>

Returns an iterator over elements satisfying the none_term_node predicate.

pub fn insert_none_term_node(&mut self, tm0: OptTermNode)

Makes none_term_node(tm0) hold.

pub fn some_term_node(&self, arg0: OptTermNode, arg1: TermNode) -> bool

Returns true if some_term_node(arg0, arg1) holds.

pub fn iter_some_term_node( &self, ) -> impl '_ + Iterator<Item = (OptTermNode, TermNode)>

Returns an iterator over tuples of elements satisfying the some_term_node predicate.

pub fn insert_some_term_node(&mut self, tm0: OptTermNode, tm1: TermNode)

Makes some_term_node(tm0, tm1) hold.

pub fn var_term_node(&self, arg0: TermNode, arg1: VirtIdent) -> bool

Returns true if var_term_node(arg0, arg1) holds.

pub fn iter_var_term_node( &self, ) -> impl '_ + Iterator<Item = (TermNode, VirtIdent)>

Returns an iterator over tuples of elements satisfying the var_term_node predicate.

pub fn insert_var_term_node(&mut self, tm0: TermNode, tm1: VirtIdent)

Makes var_term_node(tm0, tm1) hold.

pub fn wildcard_term_node(&self, arg0: TermNode) -> bool

Returns true if wildcard_term_node(arg0) holds.

pub fn iter_wildcard_term_node(&self) -> impl '_ + Iterator<Item = TermNode>

Returns an iterator over elements satisfying the wildcard_term_node predicate.

pub fn insert_wildcard_term_node(&mut self, tm0: TermNode)

Makes wildcard_term_node(tm0) hold.

pub fn app_term_node( &self, arg0: TermNode, arg1: Ident, arg2: TermListNode, ) -> bool

Returns true if app_term_node(arg0, arg1, arg2) holds.

pub fn iter_app_term_node( &self, ) -> impl '_ + Iterator<Item = (TermNode, Ident, TermListNode)>

Returns an iterator over tuples of elements satisfying the app_term_node predicate.

pub fn insert_app_term_node( &mut self, tm0: TermNode, tm1: Ident, tm2: TermListNode, )

Makes app_term_node(tm0, tm1, tm2) hold.

pub fn match_case( &self, arg0: MatchCaseNode, arg1: TermNode, arg2: StmtListNode, ) -> bool

Returns true if match_case(arg0, arg1, arg2) holds.

pub fn iter_match_case( &self, ) -> impl '_ + Iterator<Item = (MatchCaseNode, TermNode, StmtListNode)>

Returns an iterator over tuples of elements satisfying the match_case predicate.

pub fn insert_match_case( &mut self, tm0: MatchCaseNode, tm1: TermNode, tm2: StmtListNode, )

Makes match_case(tm0, tm1, tm2) hold.

pub fn nil_match_case_list_node(&self, arg0: MatchCaseListNode) -> bool

Returns true if nil_match_case_list_node(arg0) holds.

pub fn iter_nil_match_case_list_node( &self, ) -> impl '_ + Iterator<Item = MatchCaseListNode>

Returns an iterator over elements satisfying the nil_match_case_list_node predicate.

pub fn insert_nil_match_case_list_node(&mut self, tm0: MatchCaseListNode)

Makes nil_match_case_list_node(tm0) hold.

pub fn cons_match_case_list_node( &self, arg0: MatchCaseListNode, arg1: MatchCaseNode, arg2: MatchCaseListNode, ) -> bool

Returns true if cons_match_case_list_node(arg0, arg1, arg2) holds.

pub fn iter_cons_match_case_list_node( &self, ) -> impl '_ + Iterator<Item = (MatchCaseListNode, MatchCaseNode, MatchCaseListNode)>

Returns an iterator over tuples of elements satisfying the cons_match_case_list_node predicate.

pub fn insert_cons_match_case_list_node( &mut self, tm0: MatchCaseListNode, tm1: MatchCaseNode, tm2: MatchCaseListNode, )

Makes cons_match_case_list_node(tm0, tm1, tm2) hold.

pub fn equal_if_atom_node( &self, arg0: IfAtomNode, arg1: TermNode, arg2: TermNode, ) -> bool

Returns true if equal_if_atom_node(arg0, arg1, arg2) holds.

pub fn iter_equal_if_atom_node( &self, ) -> impl '_ + Iterator<Item = (IfAtomNode, TermNode, TermNode)>

Returns an iterator over tuples of elements satisfying the equal_if_atom_node predicate.

pub fn insert_equal_if_atom_node( &mut self, tm0: IfAtomNode, tm1: TermNode, tm2: TermNode, )

Makes equal_if_atom_node(tm0, tm1, tm2) hold.

pub fn defined_if_atom_node(&self, arg0: IfAtomNode, arg1: TermNode) -> bool

Returns true if defined_if_atom_node(arg0, arg1) holds.

pub fn iter_defined_if_atom_node( &self, ) -> impl '_ + Iterator<Item = (IfAtomNode, TermNode)>

Returns an iterator over tuples of elements satisfying the defined_if_atom_node predicate.

pub fn insert_defined_if_atom_node(&mut self, tm0: IfAtomNode, tm1: TermNode)

Makes defined_if_atom_node(tm0, tm1) hold.

pub fn pred_if_atom_node( &self, arg0: IfAtomNode, arg1: Ident, arg2: TermListNode, ) -> bool

Returns true if pred_if_atom_node(arg0, arg1, arg2) holds.

pub fn iter_pred_if_atom_node( &self, ) -> impl '_ + Iterator<Item = (IfAtomNode, Ident, TermListNode)>

Returns an iterator over tuples of elements satisfying the pred_if_atom_node predicate.

pub fn insert_pred_if_atom_node( &mut self, tm0: IfAtomNode, tm1: Ident, tm2: TermListNode, )

Makes pred_if_atom_node(tm0, tm1, tm2) hold.

pub fn var_if_atom_node( &self, arg0: IfAtomNode, arg1: TermNode, arg2: Ident, ) -> bool

Returns true if var_if_atom_node(arg0, arg1, arg2) holds.

pub fn iter_var_if_atom_node( &self, ) -> impl '_ + Iterator<Item = (IfAtomNode, TermNode, Ident)>

Returns an iterator over tuples of elements satisfying the var_if_atom_node predicate.

pub fn insert_var_if_atom_node( &mut self, tm0: IfAtomNode, tm1: TermNode, tm2: Ident, )

Makes var_if_atom_node(tm0, tm1, tm2) hold.

pub fn equal_then_atom_node( &self, arg0: ThenAtomNode, arg1: TermNode, arg2: TermNode, ) -> bool

Returns true if equal_then_atom_node(arg0, arg1, arg2) holds.

pub fn iter_equal_then_atom_node( &self, ) -> impl '_ + Iterator<Item = (ThenAtomNode, TermNode, TermNode)>

Returns an iterator over tuples of elements satisfying the equal_then_atom_node predicate.

pub fn insert_equal_then_atom_node( &mut self, tm0: ThenAtomNode, tm1: TermNode, tm2: TermNode, )

Makes equal_then_atom_node(tm0, tm1, tm2) hold.

pub fn defined_then_atom_node( &self, arg0: ThenAtomNode, arg1: OptTermNode, arg2: TermNode, ) -> bool

Returns true if defined_then_atom_node(arg0, arg1, arg2) holds.

pub fn iter_defined_then_atom_node( &self, ) -> impl '_ + Iterator<Item = (ThenAtomNode, OptTermNode, TermNode)>

Returns an iterator over tuples of elements satisfying the defined_then_atom_node predicate.

pub fn insert_defined_then_atom_node( &mut self, tm0: ThenAtomNode, tm1: OptTermNode, tm2: TermNode, )

Makes defined_then_atom_node(tm0, tm1, tm2) hold.

pub fn pred_then_atom_node( &self, arg0: ThenAtomNode, arg1: Ident, arg2: TermListNode, ) -> bool

Returns true if pred_then_atom_node(arg0, arg1, arg2) holds.

pub fn iter_pred_then_atom_node( &self, ) -> impl '_ + Iterator<Item = (ThenAtomNode, Ident, TermListNode)>

Returns an iterator over tuples of elements satisfying the pred_then_atom_node predicate.

pub fn insert_pred_then_atom_node( &mut self, tm0: ThenAtomNode, tm1: Ident, tm2: TermListNode, )

Makes pred_then_atom_node(tm0, tm1, tm2) hold.

pub fn if_stmt_node(&self, arg0: StmtNode, arg1: IfAtomNode) -> bool

Returns true if if_stmt_node(arg0, arg1) holds.

pub fn iter_if_stmt_node( &self, ) -> impl '_ + Iterator<Item = (StmtNode, IfAtomNode)>

Returns an iterator over tuples of elements satisfying the if_stmt_node predicate.

pub fn insert_if_stmt_node(&mut self, tm0: StmtNode, tm1: IfAtomNode)

Makes if_stmt_node(tm0, tm1) hold.

pub fn then_stmt_node(&self, arg0: StmtNode, arg1: ThenAtomNode) -> bool

Returns true if then_stmt_node(arg0, arg1) holds.

pub fn iter_then_stmt_node( &self, ) -> impl '_ + Iterator<Item = (StmtNode, ThenAtomNode)>

Returns an iterator over tuples of elements satisfying the then_stmt_node predicate.

pub fn insert_then_stmt_node(&mut self, tm0: StmtNode, tm1: ThenAtomNode)

Makes then_stmt_node(tm0, tm1) hold.

pub fn branch_stmt_node(&self, arg0: StmtNode, arg1: StmtBlockListNode) -> bool

Returns true if branch_stmt_node(arg0, arg1) holds.

pub fn iter_branch_stmt_node( &self, ) -> impl '_ + Iterator<Item = (StmtNode, StmtBlockListNode)>

Returns an iterator over tuples of elements satisfying the branch_stmt_node predicate.

pub fn insert_branch_stmt_node(&mut self, tm0: StmtNode, tm1: StmtBlockListNode)

Makes branch_stmt_node(tm0, tm1) hold.

pub fn match_stmt_node( &self, arg0: StmtNode, arg1: TermNode, arg2: MatchCaseListNode, ) -> bool

Returns true if match_stmt_node(arg0, arg1, arg2) holds.

pub fn iter_match_stmt_node( &self, ) -> impl '_ + Iterator<Item = (StmtNode, TermNode, MatchCaseListNode)>

Returns an iterator over tuples of elements satisfying the match_stmt_node predicate.

pub fn insert_match_stmt_node( &mut self, tm0: StmtNode, tm1: TermNode, tm2: MatchCaseListNode, )

Makes match_stmt_node(tm0, tm1, tm2) hold.

pub fn nil_stmt_list_node(&self, arg0: StmtListNode) -> bool

Returns true if nil_stmt_list_node(arg0) holds.

pub fn iter_nil_stmt_list_node(&self) -> impl '_ + Iterator<Item = StmtListNode>

Returns an iterator over elements satisfying the nil_stmt_list_node predicate.

pub fn insert_nil_stmt_list_node(&mut self, tm0: StmtListNode)

Makes nil_stmt_list_node(tm0) hold.

pub fn cons_stmt_list_node( &self, arg0: StmtListNode, arg1: StmtNode, arg2: StmtListNode, ) -> bool

Returns true if cons_stmt_list_node(arg0, arg1, arg2) holds.

pub fn iter_cons_stmt_list_node( &self, ) -> impl '_ + Iterator<Item = (StmtListNode, StmtNode, StmtListNode)>

Returns an iterator over tuples of elements satisfying the cons_stmt_list_node predicate.

pub fn insert_cons_stmt_list_node( &mut self, tm0: StmtListNode, tm1: StmtNode, tm2: StmtListNode, )

Makes cons_stmt_list_node(tm0, tm1, tm2) hold.

pub fn nil_stmt_block_list_node(&self, arg0: StmtBlockListNode) -> bool

Returns true if nil_stmt_block_list_node(arg0) holds.

pub fn iter_nil_stmt_block_list_node( &self, ) -> impl '_ + Iterator<Item = StmtBlockListNode>

Returns an iterator over elements satisfying the nil_stmt_block_list_node predicate.

pub fn insert_nil_stmt_block_list_node(&mut self, tm0: StmtBlockListNode)

Makes nil_stmt_block_list_node(tm0) hold.

pub fn cons_stmt_block_list_node( &self, arg0: StmtBlockListNode, arg1: StmtListNode, arg2: StmtBlockListNode, ) -> bool

Returns true if cons_stmt_block_list_node(arg0, arg1, arg2) holds.

pub fn iter_cons_stmt_block_list_node( &self, ) -> impl '_ + Iterator<Item = (StmtBlockListNode, StmtListNode, StmtBlockListNode)>

Returns an iterator over tuples of elements satisfying the cons_stmt_block_list_node predicate.

pub fn insert_cons_stmt_block_list_node( &mut self, tm0: StmtBlockListNode, tm1: StmtListNode, tm2: StmtBlockListNode, )

Makes cons_stmt_block_list_node(tm0, tm1, tm2) hold.

pub fn rule_decl(&self, arg0: RuleDeclNode, arg1: StmtListNode) -> bool

Returns true if rule_decl(arg0, arg1) holds.

pub fn iter_rule_decl( &self, ) -> impl '_ + Iterator<Item = (RuleDeclNode, StmtListNode)>

Returns an iterator over tuples of elements satisfying the rule_decl predicate.

pub fn insert_rule_decl(&mut self, tm0: RuleDeclNode, tm1: StmtListNode)

Makes rule_decl(tm0, tm1) hold.

pub fn decl_node_type(&self, arg0: DeclNode, arg1: TypeDeclNode) -> bool

Returns true if decl_node_type(arg0, arg1) holds.

pub fn iter_decl_node_type( &self, ) -> impl '_ + Iterator<Item = (DeclNode, TypeDeclNode)>

Returns an iterator over tuples of elements satisfying the decl_node_type predicate.

pub fn insert_decl_node_type(&mut self, tm0: DeclNode, tm1: TypeDeclNode)

Makes decl_node_type(tm0, tm1) hold.

pub fn decl_node_pred(&self, arg0: DeclNode, arg1: PredDeclNode) -> bool

Returns true if decl_node_pred(arg0, arg1) holds.

pub fn iter_decl_node_pred( &self, ) -> impl '_ + Iterator<Item = (DeclNode, PredDeclNode)>

Returns an iterator over tuples of elements satisfying the decl_node_pred predicate.

pub fn insert_decl_node_pred(&mut self, tm0: DeclNode, tm1: PredDeclNode)

Makes decl_node_pred(tm0, tm1) hold.

pub fn decl_node_func(&self, arg0: DeclNode, arg1: FuncDeclNode) -> bool

Returns true if decl_node_func(arg0, arg1) holds.

pub fn iter_decl_node_func( &self, ) -> impl '_ + Iterator<Item = (DeclNode, FuncDeclNode)>

Returns an iterator over tuples of elements satisfying the decl_node_func predicate.

pub fn insert_decl_node_func(&mut self, tm0: DeclNode, tm1: FuncDeclNode)

Makes decl_node_func(tm0, tm1) hold.

pub fn decl_node_rule(&self, arg0: DeclNode, arg1: RuleDeclNode) -> bool

Returns true if decl_node_rule(arg0, arg1) holds.

pub fn iter_decl_node_rule( &self, ) -> impl '_ + Iterator<Item = (DeclNode, RuleDeclNode)>

Returns an iterator over tuples of elements satisfying the decl_node_rule predicate.

pub fn insert_decl_node_rule(&mut self, tm0: DeclNode, tm1: RuleDeclNode)

Makes decl_node_rule(tm0, tm1) hold.

pub fn decl_node_enum(&self, arg0: DeclNode, arg1: EnumDeclNode) -> bool

Returns true if decl_node_enum(arg0, arg1) holds.

pub fn iter_decl_node_enum( &self, ) -> impl '_ + Iterator<Item = (DeclNode, EnumDeclNode)>

Returns an iterator over tuples of elements satisfying the decl_node_enum predicate.

pub fn insert_decl_node_enum(&mut self, tm0: DeclNode, tm1: EnumDeclNode)

Makes decl_node_enum(tm0, tm1) hold.

pub fn nil_decl_list_node(&self, arg0: DeclListNode) -> bool

Returns true if nil_decl_list_node(arg0) holds.

pub fn iter_nil_decl_list_node(&self) -> impl '_ + Iterator<Item = DeclListNode>

Returns an iterator over elements satisfying the nil_decl_list_node predicate.

pub fn insert_nil_decl_list_node(&mut self, tm0: DeclListNode)

Makes nil_decl_list_node(tm0) hold.

pub fn cons_decl_list_node( &self, arg0: DeclListNode, arg1: DeclNode, arg2: DeclListNode, ) -> bool

Returns true if cons_decl_list_node(arg0, arg1, arg2) holds.

pub fn iter_cons_decl_list_node( &self, ) -> impl '_ + Iterator<Item = (DeclListNode, DeclNode, DeclListNode)>

Returns an iterator over tuples of elements satisfying the cons_decl_list_node predicate.

pub fn insert_cons_decl_list_node( &mut self, tm0: DeclListNode, tm1: DeclNode, tm2: DeclListNode, )

Makes cons_decl_list_node(tm0, tm1, tm2) hold.

pub fn decls_module_node(&self, arg0: ModuleNode, arg1: DeclListNode) -> bool

Returns true if decls_module_node(arg0, arg1) holds.

pub fn iter_decls_module_node( &self, ) -> impl '_ + Iterator<Item = (ModuleNode, DeclListNode)>

Returns an iterator over tuples of elements satisfying the decls_module_node predicate.

pub fn insert_decls_module_node(&mut self, tm0: ModuleNode, tm1: DeclListNode)

Makes decls_module_node(tm0, tm1) hold.

pub fn var_in_scope(&self, arg0: VirtIdent, arg1: Scope) -> bool

Returns true if var_in_scope(arg0, arg1) holds.

pub fn iter_var_in_scope(&self) -> impl '_ + Iterator<Item = (VirtIdent, Scope)>

Returns an iterator over tuples of elements satisfying the var_in_scope predicate.

pub fn insert_var_in_scope(&mut self, tm0: VirtIdent, tm1: Scope)

Makes var_in_scope(tm0, tm1) hold.

pub fn scope_extension(&self, arg0: Scope, arg1: Scope) -> bool

Returns true if scope_extension(arg0, arg1) holds.

pub fn iter_scope_extension(&self) -> impl '_ + Iterator<Item = (Scope, Scope)>

Returns an iterator over tuples of elements satisfying the scope_extension predicate.

pub fn insert_scope_extension(&mut self, tm0: Scope, tm1: Scope)

Makes scope_extension(tm0, tm1) hold.

pub fn scope_single_child( &self, arg0: RuleDescendantNode, arg1: RuleDescendantNode, ) -> bool

Returns true if scope_single_child(arg0, arg1) holds.

pub fn iter_scope_single_child( &self, ) -> impl '_ + Iterator<Item = (RuleDescendantNode, RuleDescendantNode)>

Returns an iterator over tuples of elements satisfying the scope_single_child predicate.

pub fn insert_scope_single_child( &mut self, tm0: RuleDescendantNode, tm1: RuleDescendantNode, )

Makes scope_single_child(tm0, tm1) hold.

pub fn scope_extension_siblings( &self, arg0: RuleDescendantNode, arg1: RuleDescendantNode, arg2: RuleDescendantNode, ) -> bool

Returns true if scope_extension_siblings(arg0, arg1, arg2) holds.

pub fn iter_scope_extension_siblings( &self, ) -> impl '_ + Iterator<Item = (RuleDescendantNode, RuleDescendantNode, RuleDescendantNode)>

Returns an iterator over tuples of elements satisfying the scope_extension_siblings predicate.

pub fn insert_scope_extension_siblings( &mut self, tm0: RuleDescendantNode, tm1: RuleDescendantNode, tm2: RuleDescendantNode, )

Makes scope_extension_siblings(tm0, tm1, tm2) hold.

pub fn rel_app(&self, arg0: Rel, arg1: ElList) -> bool

Returns true if rel_app(arg0, arg1) holds.

pub fn iter_rel_app(&self) -> impl '_ + Iterator<Item = (Rel, ElList)>

Returns an iterator over tuples of elements satisfying the rel_app predicate.

pub fn insert_rel_app(&mut self, tm0: Rel, tm1: ElList)

Makes rel_app(tm0, tm1) hold.

pub fn el_type(&self, arg0: El, arg1: Type) -> bool

Returns true if el_type(arg0, arg1) holds.

pub fn iter_el_type(&self) -> impl '_ + Iterator<Item = (El, Type)>

Returns an iterator over tuples of elements satisfying the el_type predicate.

pub fn insert_el_type(&mut self, tm0: El, tm1: Type)

Makes el_type(tm0, tm1) hold.

pub fn el_types(&self, arg0: ElList, arg1: TypeList) -> bool

Returns true if el_types(arg0, arg1) holds.

pub fn iter_el_types(&self) -> impl '_ + Iterator<Item = (ElList, TypeList)>

Returns an iterator over tuples of elements satisfying the el_types predicate.

pub fn insert_el_types(&mut self, tm0: ElList, tm1: TypeList)

Makes el_types(tm0, tm1) hold.

pub fn constrained_el(&self, arg0: El) -> bool

Returns true if constrained_el(arg0) holds.

pub fn iter_constrained_el(&self) -> impl '_ + Iterator<Item = El>

Returns an iterator over elements satisfying the constrained_el predicate.

pub fn insert_constrained_el(&mut self, tm0: El)

Makes constrained_el(tm0) hold.

pub fn constrained_els(&self, arg0: ElList) -> bool

Returns true if constrained_els(arg0) holds.

pub fn iter_constrained_els(&self) -> impl '_ + Iterator<Item = ElList>

Returns an iterator over elements satisfying the constrained_els predicate.

pub fn insert_constrained_els(&mut self, tm0: ElList)

Makes constrained_els(tm0) hold.

pub fn in_ker(&self, arg0: Morphism, arg1: El, arg2: El) -> bool

Returns true if in_ker(arg0, arg1, arg2) holds.

pub fn iter_in_ker(&self) -> impl '_ + Iterator<Item = (Morphism, El, El)>

Returns an iterator over tuples of elements satisfying the in_ker predicate.

pub fn insert_in_ker(&mut self, tm0: Morphism, tm1: El, tm2: El)

Makes in_ker(tm0, tm1, tm2) hold.

pub fn el_in_img(&self, arg0: Morphism, arg1: El) -> bool

Returns true if el_in_img(arg0, arg1) holds.

pub fn iter_el_in_img(&self) -> impl '_ + Iterator<Item = (Morphism, El)>

Returns an iterator over tuples of elements satisfying the el_in_img predicate.

pub fn insert_el_in_img(&mut self, tm0: Morphism, tm1: El)

Makes el_in_img(tm0, tm1) hold.

pub fn rel_tuple_in_img(&self, arg0: Morphism, arg1: Rel, arg2: ElList) -> bool

Returns true if rel_tuple_in_img(arg0, arg1, arg2) holds.

pub fn iter_rel_tuple_in_img( &self, ) -> impl '_ + Iterator<Item = (Morphism, Rel, ElList)>

Returns an iterator over tuples of elements satisfying the rel_tuple_in_img predicate.

pub fn insert_rel_tuple_in_img(&mut self, tm0: Morphism, tm1: Rel, tm2: ElList)

Makes rel_tuple_in_img(tm0, tm1, tm2) hold.

pub fn defined_symbol(&self, arg0: Ident, arg1: SymbolKind, arg2: Loc) -> bool

Returns true if defined_symbol(arg0, arg1, arg2) holds.

pub fn iter_defined_symbol( &self, ) -> impl '_ + Iterator<Item = (Ident, SymbolKind, Loc)>

Returns an iterator over tuples of elements satisfying the defined_symbol predicate.

pub fn insert_defined_symbol(&mut self, tm0: Ident, tm1: SymbolKind, tm2: Loc)

Makes defined_symbol(tm0, tm1, tm2) hold.

pub fn should_be_symbol(&self, arg0: Ident, arg1: SymbolKind, arg2: Loc) -> bool

Returns true if should_be_symbol(arg0, arg1, arg2) holds.

pub fn iter_should_be_symbol( &self, ) -> impl '_ + Iterator<Item = (Ident, SymbolKind, Loc)>

Returns an iterator over tuples of elements satisfying the should_be_symbol predicate.

pub fn insert_should_be_symbol(&mut self, tm0: Ident, tm1: SymbolKind, tm2: Loc)

Makes should_be_symbol(tm0, tm1, tm2) hold.

pub fn should_be_symbol_2( &self, arg0: Ident, arg1: SymbolKind, arg2: SymbolKind, arg3: Loc, ) -> bool

Returns true if should_be_symbol_2(arg0, arg1, arg2, arg3) holds.

pub fn iter_should_be_symbol_2( &self, ) -> impl '_ + Iterator<Item = (Ident, SymbolKind, SymbolKind, Loc)>

Returns an iterator over tuples of elements satisfying the should_be_symbol_2 predicate.

pub fn insert_should_be_symbol_2( &mut self, tm0: Ident, tm1: SymbolKind, tm2: SymbolKind, tm3: Loc, )

Makes should_be_symbol_2(tm0, tm1, tm2, tm3) hold.

pub fn pred_arg_num_should_match(&self, arg0: Nat, arg1: Nat, arg2: Loc) -> bool

Returns true if pred_arg_num_should_match(arg0, arg1, arg2) holds.

pub fn iter_pred_arg_num_should_match( &self, ) -> impl '_ + Iterator<Item = (Nat, Nat, Loc)>

Returns an iterator over tuples of elements satisfying the pred_arg_num_should_match predicate.

pub fn insert_pred_arg_num_should_match(&mut self, tm0: Nat, tm1: Nat, tm2: Loc)

Makes pred_arg_num_should_match(tm0, tm1, tm2) hold.

pub fn func_arg_num_should_match(&self, arg0: Nat, arg1: Nat, arg2: Loc) -> bool

Returns true if func_arg_num_should_match(arg0, arg1, arg2) holds.

pub fn iter_func_arg_num_should_match( &self, ) -> impl '_ + Iterator<Item = (Nat, Nat, Loc)>

Returns an iterator over tuples of elements satisfying the func_arg_num_should_match predicate.

pub fn insert_func_arg_num_should_match(&mut self, tm0: Nat, tm1: Nat, tm2: Loc)

Makes func_arg_num_should_match(tm0, tm1, tm2) hold.

pub fn cfg_edge(&self, arg0: StmtNode, arg1: StmtNode) -> bool

Returns true if cfg_edge(arg0, arg1) holds.

pub fn iter_cfg_edge(&self) -> impl '_ + Iterator<Item = (StmtNode, StmtNode)>

Returns an iterator over tuples of elements satisfying the cfg_edge predicate.

pub fn insert_cfg_edge(&mut self, tm0: StmtNode, tm1: StmtNode)

Makes cfg_edge(tm0, tm1) hold.

pub fn cfg_edge_stmts_stmt(&self, arg0: StmtListNode, arg1: StmtNode) -> bool

Returns true if cfg_edge_stmts_stmt(arg0, arg1) holds.

pub fn iter_cfg_edge_stmts_stmt( &self, ) -> impl '_ + Iterator<Item = (StmtListNode, StmtNode)>

Returns an iterator over tuples of elements satisfying the cfg_edge_stmts_stmt predicate.

pub fn insert_cfg_edge_stmts_stmt(&mut self, tm0: StmtListNode, tm1: StmtNode)

Makes cfg_edge_stmts_stmt(tm0, tm1) hold.

pub fn cfg_edge_stmt_stmts(&self, arg0: StmtNode, arg1: StmtListNode) -> bool

Returns true if cfg_edge_stmt_stmts(arg0, arg1) holds.

pub fn iter_cfg_edge_stmt_stmts( &self, ) -> impl '_ + Iterator<Item = (StmtNode, StmtListNode)>

Returns an iterator over tuples of elements satisfying the cfg_edge_stmt_stmts predicate.

pub fn insert_cfg_edge_stmt_stmts(&mut self, tm0: StmtNode, tm1: StmtListNode)

Makes cfg_edge_stmt_stmts(tm0, tm1) hold.

pub fn cfg_edge_fork(&self, arg0: StmtNode, arg1: StmtBlockListNode) -> bool

Returns true if cfg_edge_fork(arg0, arg1) holds.

pub fn iter_cfg_edge_fork( &self, ) -> impl '_ + Iterator<Item = (StmtNode, StmtBlockListNode)>

Returns an iterator over tuples of elements satisfying the cfg_edge_fork predicate.

pub fn insert_cfg_edge_fork(&mut self, tm0: StmtNode, tm1: StmtBlockListNode)

Makes cfg_edge_fork(tm0, tm1) hold.

pub fn cfg_edge_join(&self, arg0: StmtBlockListNode, arg1: StmtNode) -> bool

Returns true if cfg_edge_join(arg0, arg1) holds.

pub fn iter_cfg_edge_join( &self, ) -> impl '_ + Iterator<Item = (StmtBlockListNode, StmtNode)>

Returns an iterator over tuples of elements satisfying the cfg_edge_join predicate.

pub fn insert_cfg_edge_join(&mut self, tm0: StmtBlockListNode, tm1: StmtNode)

Makes cfg_edge_join(tm0, tm1) hold.

pub fn before_stmt_structure(&self, arg0: StmtNode, arg1: Structure) -> bool

Returns true if before_stmt_structure(arg0, arg1) holds.

pub fn iter_before_stmt_structure( &self, ) -> impl '_ + Iterator<Item = (StmtNode, Structure)>

Returns an iterator over tuples of elements satisfying the before_stmt_structure predicate.

pub fn insert_before_stmt_structure(&mut self, tm0: StmtNode, tm1: Structure)

Makes before_stmt_structure(tm0, tm1) hold.

pub fn stmt_morphism(&self, arg0: StmtNode, arg1: Morphism) -> bool

Returns true if stmt_morphism(arg0, arg1) holds.

pub fn iter_stmt_morphism( &self, ) -> impl '_ + Iterator<Item = (StmtNode, Morphism)>

Returns an iterator over tuples of elements satisfying the stmt_morphism predicate.

pub fn insert_stmt_morphism(&mut self, tm0: StmtNode, tm1: Morphism)

Makes stmt_morphism(tm0, tm1) hold.

pub fn if_morphism(&self, arg0: Morphism) -> bool

Returns true if if_morphism(arg0) holds.

pub fn iter_if_morphism(&self) -> impl '_ + Iterator<Item = Morphism>

Returns an iterator over elements satisfying the if_morphism predicate.

pub fn insert_if_morphism(&mut self, tm0: Morphism)

Makes if_morphism(tm0) hold.

pub fn surj_then_morphism(&self, arg0: Morphism) -> bool

Returns true if surj_then_morphism(arg0) holds.

pub fn iter_surj_then_morphism(&self) -> impl '_ + Iterator<Item = Morphism>

Returns an iterator over elements satisfying the surj_then_morphism predicate.

pub fn insert_surj_then_morphism(&mut self, tm0: Morphism)

Makes surj_then_morphism(tm0) hold.

pub fn non_surj_then_morphism(&self, arg0: Morphism) -> bool

Returns true if non_surj_then_morphism(arg0) holds.

pub fn iter_non_surj_then_morphism(&self) -> impl '_ + Iterator<Item = Morphism>

Returns an iterator over elements satisfying the non_surj_then_morphism predicate.

pub fn insert_non_surj_then_morphism(&mut self, tm0: Morphism)

Makes non_surj_then_morphism(tm0) hold.

pub fn noop_morphism(&self, arg0: Morphism) -> bool

Returns true if noop_morphism(arg0) holds.

pub fn iter_noop_morphism(&self) -> impl '_ + Iterator<Item = Morphism>

Returns an iterator over elements satisfying the noop_morphism predicate.

pub fn insert_noop_morphism(&mut self, tm0: Morphism)

Makes noop_morphism(tm0) hold.

pub fn stmt_structure(&self, arg0: StmtNode, arg1: Structure) -> bool

Returns true if stmt_structure(arg0, arg1) holds.

pub fn iter_stmt_structure( &self, ) -> impl '_ + Iterator<Item = (StmtNode, Structure)>

Returns an iterator over tuples of elements satisfying the stmt_structure predicate.

pub fn insert_stmt_structure(&mut self, tm0: StmtNode, tm1: Structure)

Makes stmt_structure(tm0, tm1) hold.

pub fn if_atom_structure(&self, arg0: IfAtomNode, arg1: Structure) -> bool

Returns true if if_atom_structure(arg0, arg1) holds.

pub fn iter_if_atom_structure( &self, ) -> impl '_ + Iterator<Item = (IfAtomNode, Structure)>

Returns an iterator over tuples of elements satisfying the if_atom_structure predicate.

pub fn insert_if_atom_structure(&mut self, tm0: IfAtomNode, tm1: Structure)

Makes if_atom_structure(tm0, tm1) hold.

pub fn then_atom_structure(&self, arg0: ThenAtomNode, arg1: Structure) -> bool

Returns true if then_atom_structure(arg0, arg1) holds.

pub fn iter_then_atom_structure( &self, ) -> impl '_ + Iterator<Item = (ThenAtomNode, Structure)>

Returns an iterator over tuples of elements satisfying the then_atom_structure predicate.

pub fn insert_then_atom_structure(&mut self, tm0: ThenAtomNode, tm1: Structure)

Makes then_atom_structure(tm0, tm1) hold.

pub fn term_structure(&self, arg0: TermNode, arg1: Structure) -> bool

Returns true if term_structure(arg0, arg1) holds.

pub fn iter_term_structure( &self, ) -> impl '_ + Iterator<Item = (TermNode, Structure)>

Returns an iterator over tuples of elements satisfying the term_structure predicate.

pub fn insert_term_structure(&mut self, tm0: TermNode, tm1: Structure)

Makes term_structure(tm0, tm1) hold.

pub fn terms_structure(&self, arg0: TermListNode, arg1: Structure) -> bool

Returns true if terms_structure(arg0, arg1) holds.

pub fn iter_terms_structure( &self, ) -> impl '_ + Iterator<Item = (TermListNode, Structure)>

Returns an iterator over tuples of elements satisfying the terms_structure predicate.

pub fn insert_terms_structure(&mut self, tm0: TermListNode, tm1: Structure)

Makes terms_structure(tm0, tm1) hold.

pub fn opt_term_structure(&self, arg0: OptTermNode, arg1: Structure) -> bool

Returns true if opt_term_structure(arg0, arg1) holds.

pub fn iter_opt_term_structure( &self, ) -> impl '_ + Iterator<Item = (OptTermNode, Structure)>

Returns an iterator over tuples of elements satisfying the opt_term_structure predicate.

pub fn insert_opt_term_structure(&mut self, tm0: OptTermNode, tm1: Structure)

Makes opt_term_structure(tm0, tm1) hold.

pub fn term_should_be_epic_ok(&self, arg0: TermNode) -> bool

Returns true if term_should_be_epic_ok(arg0) holds.

pub fn iter_term_should_be_epic_ok(&self) -> impl '_ + Iterator<Item = TermNode>

Returns an iterator over elements satisfying the term_should_be_epic_ok predicate.

pub fn insert_term_should_be_epic_ok(&mut self, tm0: TermNode)

Makes term_should_be_epic_ok(tm0) hold.

pub fn terms_should_be_epic_ok(&self, arg0: TermListNode) -> bool

Returns true if terms_should_be_epic_ok(arg0) holds.

pub fn iter_terms_should_be_epic_ok( &self, ) -> impl '_ + Iterator<Item = TermListNode>

Returns an iterator over elements satisfying the terms_should_be_epic_ok predicate.

pub fn insert_terms_should_be_epic_ok(&mut self, tm0: TermListNode)

Makes terms_should_be_epic_ok(tm0) hold.

pub fn el_should_be_surjective_ok(&self, arg0: El) -> bool

Returns true if el_should_be_surjective_ok(arg0) holds.

pub fn iter_el_should_be_surjective_ok(&self) -> impl '_ + Iterator<Item = El>

Returns an iterator over elements satisfying the el_should_be_surjective_ok predicate.

pub fn insert_el_should_be_surjective_ok(&mut self, tm0: El)

Makes el_should_be_surjective_ok(tm0) hold.

pub fn el_is_surjective_ok(&self, arg0: El) -> bool

Returns true if el_is_surjective_ok(arg0) holds.

pub fn iter_el_is_surjective_ok(&self) -> impl '_ + Iterator<Item = El>

Returns an iterator over elements satisfying the el_is_surjective_ok predicate.

pub fn insert_el_is_surjective_ok(&mut self, tm0: El)

Makes el_is_surjective_ok(tm0) hold.

pub fn should_be_obtained_by_ctor( &self, arg0: TermNode, arg1: EnumDeclNode, ) -> bool

Returns true if should_be_obtained_by_ctor(arg0, arg1) holds.

pub fn iter_should_be_obtained_by_ctor( &self, ) -> impl '_ + Iterator<Item = (TermNode, EnumDeclNode)>

Returns an iterator over tuples of elements satisfying the should_be_obtained_by_ctor predicate.

pub fn insert_should_be_obtained_by_ctor( &mut self, tm0: TermNode, tm1: EnumDeclNode, )

Makes should_be_obtained_by_ctor(tm0, tm1) hold.

pub fn is_given_by_ctor(&self, arg0: TermNode, arg1: EnumDeclNode) -> bool

Returns true if is_given_by_ctor(arg0, arg1) holds.

pub fn iter_is_given_by_ctor( &self, ) -> impl '_ + Iterator<Item = (TermNode, EnumDeclNode)>

Returns an iterator over tuples of elements satisfying the is_given_by_ctor predicate.

pub fn insert_is_given_by_ctor(&mut self, tm0: TermNode, tm1: EnumDeclNode)

Makes is_given_by_ctor(tm0, tm1) hold.

pub fn function_can_be_made_defined(&self, arg0: Func) -> bool

Returns true if function_can_be_made_defined(arg0) holds.

pub fn iter_function_can_be_made_defined( &self, ) -> impl '_ + Iterator<Item = Func>

Returns an iterator over elements satisfying the function_can_be_made_defined predicate.

pub fn insert_function_can_be_made_defined(&mut self, tm0: Func)

Makes function_can_be_made_defined(tm0) hold.

pub fn case_pattern_is_variable(&self, arg0: Loc) -> bool

Returns true if case_pattern_is_variable(arg0) holds.

pub fn iter_case_pattern_is_variable(&self) -> impl '_ + Iterator<Item = Loc>

Returns an iterator over elements satisfying the case_pattern_is_variable predicate.

pub fn insert_case_pattern_is_variable(&mut self, tm0: Loc)

Makes case_pattern_is_variable(tm0) hold.

pub fn case_pattern_is_wildcard(&self, arg0: Loc) -> bool

Returns true if case_pattern_is_wildcard(arg0) holds.

pub fn iter_case_pattern_is_wildcard(&self) -> impl '_ + Iterator<Item = Loc>

Returns an iterator over elements satisfying the case_pattern_is_wildcard predicate.

pub fn insert_case_pattern_is_wildcard(&mut self, tm0: Loc)

Makes case_pattern_is_wildcard(tm0) hold.

pub fn is_pattern_ctor_arg(&self, arg0: TermNode) -> bool

Returns true if is_pattern_ctor_arg(arg0) holds.

pub fn iter_is_pattern_ctor_arg(&self) -> impl '_ + Iterator<Item = TermNode>

Returns an iterator over elements satisfying the is_pattern_ctor_arg predicate.

pub fn insert_is_pattern_ctor_arg(&mut self, tm0: TermNode)

Makes is_pattern_ctor_arg(tm0) hold.

pub fn are_pattern_ctor_args(&self, arg0: TermListNode) -> bool

Returns true if are_pattern_ctor_args(arg0) holds.

pub fn iter_are_pattern_ctor_args( &self, ) -> impl '_ + Iterator<Item = TermListNode>

Returns an iterator over elements satisfying the are_pattern_ctor_args predicate.

pub fn insert_are_pattern_ctor_args(&mut self, tm0: TermListNode)

Makes are_pattern_ctor_args(tm0) hold.

pub fn pattern_ctor_arg_is_app(&self, arg0: Loc) -> bool

Returns true if pattern_ctor_arg_is_app(arg0) holds.

pub fn iter_pattern_ctor_arg_is_app(&self) -> impl '_ + Iterator<Item = Loc>

Returns an iterator over elements satisfying the pattern_ctor_arg_is_app predicate.

pub fn insert_pattern_ctor_arg_is_app(&mut self, tm0: Loc)

Makes pattern_ctor_arg_is_app(tm0) hold.

pub fn pattern_ctor_arg_var_is_not_fresh(&self, arg0: Loc) -> bool

Returns true if pattern_ctor_arg_var_is_not_fresh(arg0) holds.

pub fn iter_pattern_ctor_arg_var_is_not_fresh( &self, ) -> impl '_ + Iterator<Item = Loc>

Returns an iterator over elements satisfying the pattern_ctor_arg_var_is_not_fresh predicate.

pub fn insert_pattern_ctor_arg_var_is_not_fresh(&mut self, tm0: Loc)

Makes pattern_ctor_arg_var_is_not_fresh(tm0) hold.

pub fn cases_contain_ctor( &self, arg0: MatchCaseListNode, arg1: CtorDeclNode, ) -> bool

Returns true if cases_contain_ctor(arg0, arg1) holds.

pub fn iter_cases_contain_ctor( &self, ) -> impl '_ + Iterator<Item = (MatchCaseListNode, CtorDeclNode)>

Returns an iterator over tuples of elements satisfying the cases_contain_ctor predicate.

pub fn insert_cases_contain_ctor( &mut self, tm0: MatchCaseListNode, tm1: CtorDeclNode, )

Makes cases_contain_ctor(tm0, tm1) hold.

pub fn match_stmt_contains_ctor_of_enum( &self, arg0: StmtNode, arg1: CtorDeclNode, arg2: EnumDeclNode, ) -> bool

Returns true if match_stmt_contains_ctor_of_enum(arg0, arg1, arg2) holds.

pub fn iter_match_stmt_contains_ctor_of_enum( &self, ) -> impl '_ + Iterator<Item = (StmtNode, CtorDeclNode, EnumDeclNode)>

Returns an iterator over tuples of elements satisfying the match_stmt_contains_ctor_of_enum predicate.

pub fn insert_match_stmt_contains_ctor_of_enum( &mut self, tm0: StmtNode, tm1: CtorDeclNode, tm2: EnumDeclNode, )

Makes match_stmt_contains_ctor_of_enum(tm0, tm1, tm2) hold.

pub fn match_stmt_should_contain_ctor( &self, arg0: StmtNode, arg1: CtorDeclNode, ) -> bool

Returns true if match_stmt_should_contain_ctor(arg0, arg1) holds.

pub fn iter_match_stmt_should_contain_ctor( &self, ) -> impl '_ + Iterator<Item = (StmtNode, CtorDeclNode)>

Returns an iterator over tuples of elements satisfying the match_stmt_should_contain_ctor predicate.

pub fn insert_match_stmt_should_contain_ctor( &mut self, tm0: StmtNode, tm1: CtorDeclNode, )

Makes match_stmt_should_contain_ctor(tm0, tm1) hold.

pub fn match_stmt_contains_ctor( &self, arg0: StmtNode, arg1: CtorDeclNode, ) -> bool

Returns true if match_stmt_contains_ctor(arg0, arg1) holds.

pub fn iter_match_stmt_contains_ctor( &self, ) -> impl '_ + Iterator<Item = (StmtNode, CtorDeclNode)>

Returns an iterator over tuples of elements satisfying the match_stmt_contains_ctor predicate.

pub fn insert_match_stmt_contains_ctor( &mut self, tm0: StmtNode, tm1: CtorDeclNode, )

Makes match_stmt_contains_ctor(tm0, tm1) hold.

Trait Implementations

impl Clone for Eqlog

fn clone(&self) -> Eqlog

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Eqlog

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for Eqlog

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.