		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-implementation

Deftreeops-event-generation

Event generation performed by deftreeops.

Subtopics

Deftreeops-gen-rep-events: Generate the functions and theorems for a repetition in a concatenation in the alternation that defines a rule name.
Deftreeops-gen-conc-events: Generate the functions and theorems for a concatenation in the alternation that defines a rule name.
Deftreeops-gen-rulename-events: Generate the events for a rule name.
Deftreeops-gen-rulename-alist-events: Generate the events for all the rule names in the alist.
Deftreeops-gen-discriminant-terms: Generate the terms to discriminate among two or more concatenations that form the alternation that defines a rule name.
Deftreeops-gen-conc-list-events: Lift deftreeops-gen-conc-events to lists.
Deftreeops-gen-rep-list-events: Lift deftreeops-gen-rep-events to lists.
Deftreeops-gen-numrange-events: Generate the function and theorem for a numeric range.
Deftreeops-gen-conc-info-list: Lift deftreeops-gen-conc-info to lists of concatenations, i.e. to alternations.
Deftreeops-gen-cst-list-list-conc-match: Generate the fourth of the specialized matching predicates.
Deftreeops-gen-cst-list-list-alt-match: Generate the fifth of the specialized matching predicates.
Deftreeops-gen-conc-info: Generate the information for a concatenation in the alternation that defines a rule name.
Deftreeops-gen-all-rulename-infos+events: Generate the information and events for all the rulenames in a grammar.
Deftreeops-gen-rep-info: Generate the information for a repetition in a concatenation in the alternation that defines a rule name.
Deftreeops-gen-cst-list-rep-match: Generate the third of the specialized matching predicates.
Deftreeops-gen-cst-list-elem-match: Generate the second of the specialized matching predicates.
Deftreeops-gen-rulename-info-alist: Generate the alist from rule names to rule name information, from a list of rules.
Deftreeops-gen-cst-match: Generate the first of the specialized matching predicates.
Deftreeops-gen-charval-events: Generate the theorem for a character value notation.
Deftreeops-gen-numrange-alist-events: Generate the events for all the numeric ranges in the alist.
Deftreeops-gen-all-numrange-infos+events: Generate the information and events for all the numeric ranges in a grammar.
Deftreeops-gen-all-charval-infos+events: Generate the information and events for all the character value notations in a grammar.
Deftreeops-gen-everything: Generate all the events.
Deftreeops-gen-charval-alist-events: Generate the events for all the character value notations in the alist.
Deftreeops-gen-charval-info-alist: Generate the alist from character value notation to character value notation information from a list of rules.
Deftreeops-gen-rulename-info: Generate the information for a rule name.
Deftreeops-gen-rep-info-list: Lift deftreeops-gen-rep-info to lists of repetitions, i.e. to concatenations.
Deftreeops-gen-numrange-info-alist: Generate the alist from numeric ranges to numeric range information, from a list of rules.
Deftreeops-gen-matchers: Generate the specialized matching predicates.
Deftreeops-gen-numrange-info: Generate the information for a numeric range.
Deftreeops-gen-charval-info: Generate the information for a character value notation.
Deftreeops-elem-match-pred: Name of the <prefix>-list-elem-matchp predicate.
Deftreeops-conc-match-pred: Name of the <prefix>-list-list-conc-matchp predicate.
Deftreeops-alt-match-pred: Name of the <prefix>-list-list-alt-matchp predicate.
Deftreeops-rep-match-pred: Name of the <prefix>-list-rep-matchp predicate.
Deftreeops-match-pred: Name of the <prefix>-matchp predicate.