KeYProject / key

KeY Theorem Prover for Deductive Java Verification
https://key-project.org
Other
41 stars 24 forks source link

Revive work on Polymorphic Sorts #3384

Open wadoon opened 8 months ago

wadoon commented 8 months ago

Introducing Sorts with Sort-Parameters.

Type of pull request

wadoon commented 8 months ago

Support for data types:

\sorts{\generic E;} \datatypes { List<[E]> = Nil | Cons(E obj, List<[E]> tail);

Test case fails.

mattulbrich commented 2 months ago

There are a number of fundamental questions to be sorted out: https://github.com/KeYProject/key/wiki/Polymorphic-types-in-KeY