11 Commits

Author	SHA1	Message	Date
Patrick Lühne	491a255811	Require supertight programs for backward proof	2020-05-28 05:03:56 +02:00
Patrick Lühne	739cae1f7c	Rename “assert” statement to “spec”	2020-05-22 18:34:59 +02:00
Patrick Lühne	81ddfd450a	Use custom foliage flavor ... With this patch, properties specific to variable, function, and predicate declarations are directly stored within those objects rather than external maps that need to be queried via traits. This greatly simplifies many parts of the logic. This is made possible by implementing a custom foliage flavor, which makes it possible to swap the built-in declaration types for extended versions of those types that fulfill certain requirements.	2020-05-22 02:25:00 +02:00
Patrick Lühne	efe354faad	Clean up unused struct	2020-05-19 13:02:12 +02:00
Patrick Lühne	efa5656e39	Clean up unused struct	2020-05-19 13:01:04 +02:00
Patrick Lühne	d77c7648b3	Ensure that statements are proven in right order	2020-05-19 12:56:21 +02:00
Patrick Lühne	b308847ebd	Add to-do note	2020-05-13 03:17:37 +02:00
Patrick Lühne	d35d0d1d98	Use statement kind over section kind	2020-05-13 03:17:33 +02:00
Patrick Lühne	2de8a59b63	New output format	2020-05-11 05:03:59 +02:00
Patrick Lühne	0d51053b88	Move ProofDirection type to separate module	2020-05-11 03:46:11 +02:00
Patrick Lühne	17d2373e0d	Refactor proof output	2020-05-11 03:11:10 +02:00