Subtraction is too hard for PL people, it is better left to pupils in a Grundschule. Therefore, we should aim to never subtract in our code. This merge request removes some spurious subtractions that were introduced due to a Coq quirk.
We also do the same in systemf_mu_state
Very neat, thank you!
Subtraction is too hard for PL people, it is better left to pupils in a Grundschule. Therefore, we should aim to never subtract in our code. This merge request removes some spurious subtractions that were introduced due to a Coq quirk.
We also do the same in systemf_mu_state
Lennard Gäher (70a6a070) at 04 Oct 06:28
bump ci to 8.18
Lennard Gäher (f4d2aa12) at 04 Oct 06:25
bump
Lennard Gäher (8fb53998) at 07 Jun 08:05
update license
Lennard Gäher (19a16b79) at 26 May 08:23
fix comment
Lennard Gäher (7a7a84d9) at 26 May 08:22
update iris
Lennard Gäher (945ce808) at 26 May 08:22
update ci to 8.17
Lennard Gäher (2b18ebd3) at 18 Mar 13:12
bump Iris
Lennard Gäher (50b5b17a) at 09 Mar 13:23
bump iris
Lennard Gäher (152eaab9) at 30 Nov 08:16
bump iris
Lennard Gäher (93950e22) at 26 Nov 10:06
bump iris
Lennard Gäher (3acfa14a) at 29 Sep 08:15
bump iris and move ci to 8.16
Lennard Gäher (f9b4c753) at 22 Sep 16:43
adapt for Coq 8.16
Lennard Gäher (32f0455e) at 22 Sep 16:06
bump iris
Lennard Gäher (120e9af9) at 14 Aug 08:54
bump iris
Lennard Gäher (f5867e78) at 09 Aug 07:20
bump iris
Lennard Gäher (887ba93d) at 29 Jul 13:12
opam metadata