- (* an inductive predicate proving that a given computation terminates with /some/ value *)
- Inductive Terminates (A:Set) : #A -> Prop :=
- | TerminatesReturn :
- forall (a:A),
- Terminates A (Return a)
-
- | TerminatesBind :
- forall (B:Set) (f:B->#A) (c:#B),
- Terminates B c
- -> (forall (b:B), (TerminatesWith B c b) -> Terminates A (f b))
- -> Terminates A (@Bind A B f c)
- .
+ (* an inductive predicate proving that a given computation terminates with /some/ value *)
+ Reserved Notation "c !?" (at level 30).
+ Inductive Terminates (A:Set)(c:#A) : Prop :=
+ | Terminates_intro : (exists a:A, c!a) -> c!?
+ where "c !?" := (Terminates _ c).