Mercurial > cpdt > repo

comparison src/Match.v @ 205:f05514cc6c0d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
'make doc' works with 8.2
author Adam Chlipala <adamc@hcoop.net>
date Fri, 06 Nov 2009 12:15:05 -0500
parents cbf2f74a5130
children 15501145d696
comparison
equal deleted inserted replaced
204:cbf2f74a5130 205:f05514cc6c0d
87 Hint Extern 1 (?P ?X) => 87 Hint Extern 1 (?P ?X) =>
88 match goal with 88 match goal with
89 | [ H : forall x, ?P x /\ _ |- _ ] => apply (proj1 (H X)) 89 | [ H : forall x, ?P x /\ _ |- _ ] => apply (proj1 (H X))
90 end. 90 end.
91 91
92 ]]
93
92 [[ 94 [[
93 User error: Bound head variable 95 User error: Bound head variable
94 ]] 96 ]]
95 97
96 Coq's [auto] hint databases work as tables mapping %\textit{%#<i>#head symbols#</i>#%}% to lists of tactics to try. Because of this, the constant head of an [Extern] pattern must be determinable statically. In our first [Extern] hint, the head symbol was [not], since [x <> y] desugars to [not (eq x y)]; and, in the second example, the head symbol was [P]. 98 Coq's [auto] hint databases work as tables mapping %\textit{%#<i>#head symbols#</i>#%}% to lists of tactics to try. Because of this, the constant head of an [Extern] pattern must be determinable statically. In our first [Extern] hint, the head symbol was [not], since [x <> y] desugars to [not (eq x y)]; and, in the second example, the head symbol was [P].
448 (* begin thide *) 450 (* begin thide *)
449 (** [[ 451 (** [[
450 452
451 completer'. 453 completer'.
452 454
455 ]]
456
453 Coq loops forever at this point. What went wrong? *) 457 Coq loops forever at this point. What went wrong? *)
454 Abort. 458 Abort.
455 (* end thide *) 459 (* end thide *)
456 End firstorder'. 460 End firstorder'.
457 461
472 (** [[ 476 (** [[
473 477
474 match goal with 478 match goal with
475 | [ |- forall x, ?P ] => trivial 479 | [ |- forall x, ?P ] => trivial
476 end. 480 end.
481
482 ]]
477 483
478 [[ 484 [[
479 User error: No matching clauses for match goal 485 User error: No matching clauses for match goal
480 ]] *) 486 ]] *)
481 Abort. 487 Abort.
501 match ls with 507 match ls with
502 | nil => O 508 | nil => O
503 | _ :: ls' => S (length ls') 509 | _ :: ls' => S (length ls')
504 end. 510 end.
505 511
512 ]]
513
506 [[ 514 [[
507 Error: The reference ls' was not found in the current environment 515 Error: The reference ls' was not found in the current environment
508 ]] 516 ]]
509 517
510 At this point, we hopefully remember that pattern variable names must be prefixed by question marks in Ltac. 518 At this point, we hopefully remember that pattern variable names must be prefixed by question marks in Ltac.
513 Ltac length ls := 521 Ltac length ls :=
514 match ls with 522 match ls with
515 | nil => O 523 | nil => O
516 | _ :: ?ls' => S (length ls') 524 | _ :: ?ls' => S (length ls')
517 end. 525 end.
526
527 ]]
518 528
519 [[ 529 [[
520 Error: The reference S was not found in the current environment 530 Error: The reference S was not found in the current environment
521 ]] 531 ]]
522 532