Revision 4c564f5656282f56fe4bb433bc0b49d789330ee6 authored by Pierre-Yves Strub on 06 December 2023, 10:56:36 UTC, committed by Pierre-Yves Strub on 11 December 2023, 12:52:51 UTC
This family of functions type-check a formula w.r.t. a memory that is infered from the program logic goal. The commit changes two things: - for prhl, its uses the same memory name as the one used in the program logic goal. (Previously, it was using `mhr`) - its returns the memory that has been used for the type-checking
1 parent 4f02829
Computing file changes ...
