Commit 9d1092a0 authored by Robbert Krebbers's avatar Robbert Krebbers

Unfolding lemma for Acc.

parent 8497827e
......@@ -198,6 +198,9 @@ Notation wf := well_founded.
Section wf.
Context `{R : relation A}.
Lemma Acc_def x : Acc R x ( y : A, R y x Acc R y).
Proof. split. by destruct 1. by constructor. Qed.
(** A trick by Thomas Braibant to compute with well-founded recursions:
it lazily adds [2^n] [Acc_intro] constructors in front of a well foundedness
proof, so that the actual proof is never reached in practise. *)
......
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