KeY Logic Documentation

Defined symbols in the KeY System

Generated from version: heads/main on Sat Mar 01 14:33:17 UTC 2025

Overview

wellfound.key

Sorts

Pair

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

Functions

pair

\unique Pair pair (any , any ); defined in: wellfound.key Line: 29 Offset :4

first

any first (Pair ); defined in: wellfound.key Line: 30 Offset :4

second

any second (Pair ); defined in: wellfound.key Line: 31 Offset :4

Predicates

prec

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

measuredBy

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

measuredByEmpty

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

measuredByCheck

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