Mercurial > cpdt > repo

comparison src/MoreDep.v @ 89:939add5a7db9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Remove -impredicative-set
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Oct 2008 10:49:07 -0400
parents a0b8b550e265
children 4a57a4922af5
comparison
equal deleted inserted replaced
88:cde1351d18bb 89:939add5a7db9
347 (** * A Certified Regular Expression Matcher *) 347 (** * A Certified Regular Expression Matcher *)
348 348
349 Require Import Ascii String. 349 Require Import Ascii String.
350 Open Scope string_scope. 350 Open Scope string_scope.
351 351
352 Inductive regexp : (string -> Prop) -> Set := 352 Inductive regexp : (string -> Prop) -> Type :=
353 | Char : forall ch : ascii, 353 | Char : forall ch : ascii,
354 regexp (fun s => s = String ch "") 354 regexp (fun s => s = String ch "")
355 | Concat : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2), 355 | Concat : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),
356 regexp (fun s => exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2) 356 regexp (fun s => exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2)
357 | Or : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2), 357 | Or : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),