Automatischen Terminierungsnachweis erstellen, andere Größenfunktion verwenden
Ich habe eine benutzerdefinierte Größenfunktion geschriebensize2
für meinen Datentyp. Mit dieser Funktion kann ich die Beendigung meiner Funktion manuell nachweisen:
termination
apply (relation "measure (λ(a,b,c). size2 c)")
apply auto
done
Gibt es eine Möglichkeit, @ zu machfun
Meine alternative Größenfunktion für den automatischen Terminierungsnachweis verwenden?