Sorted Terms

Akihisa Yamada 📧 and René Thiemann 🌐

May 27, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


This entry provides a basic library for many-sorted terms and algebras. We view sorted sets just as partial maps from elements to sorts, and define sorted set of terms reusing the data type from the existing library of (unsorted) first order terms. All the existing functionality, such as substitutions and contexts, can be reused without any modifications. We provide predicates stating what substitutions or contexts are considered sorted, and prove facts that they preserve sorts as expected.


BSD License


Session Sorted_Terms