From 9ce6a85d86cdc3a5bba1f5c3cd153cdc046f10b9 Mon Sep 17 00:00:00 2001 From: adam Date: Sun, 28 Oct 2007 22:24:07 +0000 Subject: [PATCH] add example showing why we cannot simply extract the witness from TerminatesWith to get a trivial eval darcs-hash:20071028222407-5007d-35f02a37ae798d87d4dc41385d07f6a687c1b2d3.gz --- Computation/Eval.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) 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 -- 1.7.10.4