KeY Logic Documentation

Defined symbols in the KeY System

Generated from version: heads/main on Fri Aug 21 01:50:47 UTC 2026

Overview

wellfound.key

Sorts

Pair

Pair;defined in: wellfound.key Line: 24 Offset :4

Functions

pair

Return the (unique) ordered pair of two specified elements.

/*! Return the (unique) ordered pair of two specified elements. */ \unique Pair pair ( any , any ) ; defined in: wellfound.key Line: 29 Offset :4

first

Return the first element of an ordered pair.

/*! Return the first element of an ordered pair. */ any first ( Pair ) ; defined in: wellfound.key Line: 32 Offset :4

second

Return the second element of an ordered pair.

/*! Return the second element of an ordered pair. */ any second ( Pair ) ; defined in: wellfound.key Line: 35 Offset :4

Predicates

prec

prec ( any , any ) ; defined in: wellfound.key Line: 40 Offset :4

measuredBy

measuredBy ( any ) ; defined in: wellfound.key Line: 41 Offset :4

measuredByEmpty

measuredByEmpty ; defined in: wellfound.key Line: 42 Offset :4

measuredByCheck

measuredByCheck ( any ) ; defined in: wellfound.key Line: 43 Offset :4