Commit 3777800c authored by Florian Rabe's avatar Florian Rabe

no message

parent fe7d1a19
......@@ -175,7 +175,8 @@ theory ResourceSemantics : /examples?FOLEQNatDed =
([b,q] !_L q ([qE] !_R (⊕_Rr qE)))❙
!_over_& : {A,B} valid !(A&B) ⊸ (!A&!B)❘
// TODO: This proof unexpectedly does not type-check, eventually failing at a=ε and b=ε.
Further investigation is needed to determine if the proof is in fat wrong or if the type-checker is led astray by the EquateWorlds rules.❙
Further investigation is needed to determine if the proof is in fact wrong or
if the type-checker is led astray by the EquateWorlds rule.❙
// = [A,B] ⊸_R [ab,h] &_R (!_L h [pqE] &_Ll pqE ([a,p] !_R p))
(!_L h [pqE] &_Lr pqE ([b,q] !_R q))❙
!_idempotent1 : {A} valid !!A ⊸ !A❘
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment