Abstract
This theory provides functions for finding the index of an element in a list, by predicate and by value.
BSD LicenseUsed by
- Fishers_Inequality
- Gale_Shapley
- Dominance_CHK
- Metalogic_ProofChecker
- JinjaDCI
- Verified_SAT_Based_AI_Planning
- Smith_Normal_Form
- Higher_Order_Terms
- Comparison_Sort_Lower_Bound
- Quick_Sort_Cost
- Nested_Multisets_Ordinals
- Refine_Imperative_HOL
- Randomised_Social_Choice
- List_Update
- Planarity_Certificates
- LTL_to_DRA
- Formula_Derivatives
- MSO_Regex_Equivalence
- Affine_Arithmetic
- Ordinary_Differential_Equations
- Jinja