diff options
author | 2009-02-21 13:22:30 -0500 | |
---|---|---|
committer | 2009-02-21 13:22:30 -0500 | |
commit | a7cfb825cdfa5ed9ea77598b20e432caa49d8a5a (patch) | |
tree | 1ffa812bdb1fcfc087d3c83b948c32f66023ebc8 /src/coq/Semantics.v | |
parent | e4b9964e2f79cac5eff8ef728560cc539d256cb3 (diff) |
Time to start thinking about guards
Diffstat (limited to 'src/coq/Semantics.v')
-rw-r--r-- | src/coq/Semantics.v | 16 |
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. |