Mercurial > urweb

comparison src/coq/Semantics.v @ 619:f38e009009bb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Time to start thinking about guards
author Adam Chlipala <adamc@hcoop.net>
date Sat, 21 Feb 2009 13:22:30 -0500
parents be88d2d169f6
children d828b143e147
comparison
equal deleted inserted replaced
618:be88d2d169f6 619:f38e009009bb
207 end 207 end
208 end 208 end
209 | right _ => fun x => x 209 | right _ => fun x => x
210 end ((eDen e1) n) 210 end ((eDen e1) n)
211 211
212 | Concat c1 c2 e1 e2 => fun n =>
213 match (cDen c1) n as D return match D with
214 | None => unit
215 | Some T => T
216 end
217 -> match (match D with
218 | None => (cDen c2) n
219 | v => v
220 end) with
221 | None => unit
222 | Some T => T
223 end with
224 | None => fun _ => (eDen e2) n
225 | _ => fun x => x
226 end ((eDen e1) n)
227
212 | _ => cheat _ 228 | _ => cheat _
213 end. 229 end.