summaryrefslogtreecommitdiff
path: root/src/coq/Semantics.v
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-02-21 13:22:30 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-02-21 13:22:30 -0500
commitfe5ac0fba7f973b2557c7ae7a6bb9248024ffacd (patch)
tree1ffa812bdb1fcfc087d3c83b948c32f66023ebc8 /src/coq/Semantics.v
parent8794ce0f4d86c23e15314141e3638d99277e2ad0 (diff)
Time to start thinking about guards
Diffstat (limited to 'src/coq/Semantics.v')
-rw-r--r--src/coq/Semantics.v16
1 files changed, 16 insertions, 0 deletions
diff --git a/src/coq/Semantics.v b/src/coq/Semantics.v
index 2022ec94..19c67a05 100644
--- a/src/coq/Semantics.v
+++ b/src/coq/Semantics.v
@@ -209,5 +209,21 @@ Fixpoint eDen t (e : exp dvar tDen t) {struct e} : tDen t :=
| right _ => fun x => x
end ((eDen e1) n)
+ | Concat c1 c2 e1 e2 => fun n =>
+ match (cDen c1) n as D return match D with
+ | None => unit
+ | Some T => T
+ end
+ -> match (match D with
+ | None => (cDen c2) n
+ | v => v
+ end) with
+ | None => unit
+ | Some T => T
+ end with
+ | None => fun _ => (eDen e2) n
+ | _ => fun x => x
+ end ((eDen e1) n)
+
| _ => cheat _
end.