Legend:
 Unmodified
 Added
 Removed

LTS/Vm.ma
r3552 r3563 3 3 include "../src/utilities/option.ma". 4 4 include "basics/jmeq.ma". 5 6 lemma bind_inversion : ∀A,B : Type[0].∀m : option A.7 ∀f : A → option B.∀y : B.8 ! x ← m; f x = return y →9 ∃ x.(m = return x) ∧ (f x = return y).10 #A #B * [ #a] #f #y normalize #EQ [destruct]11 %{a} %{(refl …)} //12 qed.13 5 14 6 record assembler_params : Type[1] ≝
Note: See TracChangeset
for help on using the changeset viewer.