From: adam
Date: Sun, 28 Oct 2007 22:24:07 +0000 (+0000)
Subject: add example showing why we cannot simply extract the witness from TerminatesWith...
X-Git-Url: http://git.megacz.com/?p=coinductive-monad.git;a=commitdiff_plain;h=9ce6a85d86cdc3a5bba1f5c3cd153cdc046f10b9
add example showing why we cannot simply extract the witness from TerminatesWith to get a trivial eval
darcs-hash:20071028222407-5007d-35f02a37ae798d87d4dc41385d07f6a687c1b2d3.gz
---
diff --git a/Computation/Eval.v b/Computation/Eval.v
index 07d79e4..28a00a0 100644
--- a/Computation/Eval.v
+++ b/Computation/Eval.v
@@ -17,6 +17,25 @@ Fixpoint bounded_eval (A:Set) (n:nat) (c:#A) {struct n} : option A :=
end.
Inductive Unit : Set := unit : Unit.
+
+(*
+ * In theory we'd like to be able to do this (below), but it violates
+ * the Prop/Set separation:
+ *
+ * "Elimination of an inductive object of sort Prop is not allowed on a
+ * predicate in sort Set because proofs can be eliminated only to
+ * build proofs."
+ *)
+(*
+Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
+ match t with
+ | (Terminates_intro t') =>
+ match t' with
+ | (ex_intro x y) => x
+ end
+ end.
+*)
+
Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
match eval' c Unit (Return unit) (termination_is_safe A c t) with
| exist x pf => x