Skip to content

Rules for fancy updates and plain propositions.

Robbert Krebbers requested to merge fupd_plain into master

This addresses #105 (closed). I have tweaked @amintimany code a bit: the statements are no entirely in the logic, and secondly, I shortened the proofs.

@jung had some suggestions for simpler rules; can you check with @amintimany whether these are sufficient.

Fixes: #105 (closed)

Edited by Ralf Jung

Merge request reports