diff options
Diffstat (limited to 'theories/Program/Wf.v')
| -rw-r--r-- | theories/Program/Wf.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index 6278798543..8479b9a2bb 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -32,6 +32,8 @@ Section Well_founded. Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x). + Register Fix_sub as program.wf.fix_sub. + (* Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *) *) (* Definition Fix (x:A) := Fix_F_sub P F_sub x (Rwf x). *) @@ -89,6 +91,8 @@ Section Measure_well_founded. Definition MR (x y: T): Prop := R (m x) (m y). + Register MR as program.wf.mr. + Lemma measure_wf: well_founded MR. Proof with auto. unfold well_founded. |