[INCLUDE TH/speedbar.blogme]
[# 
(defun c () (interactive) (find-blogme3-sh0-if "coq"))
;;    http://angg.twu.net/coq.html
;; file:///home/edrx/TH/L/coq.html
;; (eev-traffic-light-glyphs)
(defun fr () (interactive)
  (fooi-re "\n\\([^\n<]+<\\)\\([^\n]*\\)" "\n
\\1\\2"))

#]
[SETFAVICON eev-current/eev-icon.png]

[htmlize [J Coq]

[_TARGETS
  coq.e            -> (find-es "coq")
  coq-tutorial     -> (find-es "coq" "coq-tutorial")
  tutorial.html    -> (find-coqv81w3m "tutorial.html")
  tutorial.html#Ex -> (find-coqv81w3m "tutorial.html#htoc13")
  eepitch          -> (find-eevarticlesection "eepitch")
  e-script         -> (find-eevarticlesection "e-scripts")
  eev-tutorial     -> (find-TH "emacs" "short-eev-tutorial")

]

[P At this moment I am just trying to run the code in the [__
tutorial.html Coq Tutorial]...]

[P The [__ coq-tutorial following] [_ e-script], corresponding to the
section "[__ tutorial.html#Ex Existential Quantification]" of the
tutorial, is not working as it should:]

[BE'
;; (find-coqv81w3m "tutorial.html#htoc12" "Sections and signatures")
 (eepitch-coqtop)
 (eepitch-kill)
 (eepitch-coqtop)
Reset Initial.
Section Predicate_calculus.
Variable D : Set.
Variable R : D -> D -> Prop.
Section R_sym_trans.
Hypothesis R_symmetric : forall x y:D, R x y -> R y x.
Hypothesis R_transitive : forall x y z:D, R x y -> R y z -> R x z.
Lemma refl_if : forall x:D, (exists y, R x y) -> R x x.
Check ex.
intros x x_Rlinked.
intro y.
]

[P Here is its log:]

[PRE [TRAFFIC ['
Welcome to Coq 8.1pl3 (Dec. 2007)]


Coq < Reset Initial.


Coq < Section Predicate_calculus.


Coq < Variable D : Set.
D is assumed


Coq < Variable R : D -> D -> Prop.
R is assumed


Coq < Section R_sym_trans.


Coq < Hypothesis R_symmetric : forall x y:D, R x y -> R y x.
R_symmetric is assumed


Coq < Hypothesis R_transitive : forall x y z:D, R x y -> R y z -> R x z.
R_transitive is assumed


Coq < Lemma refl_if : forall x:D, (exists y, R x y) -> R x x.
1 subgoal
  
  D : Set
  R : D -> D -> Prop
  R_symmetric : forall x y : D, R x y -> R y x
  R_transitive : forall x y z : D, R x y -> R y z -> R x z
  ============================
   forall x : D, (exists y : D, R x y) -> R x x


refl_if < Check ex.
ex
     : forall A : Type, (A -> Prop) -> Prop


refl_if < intros x x_Rlinked.
1 subgoal
  
  D : Set
  R : D -> D -> Prop
  R_symmetric : forall x y : D, R x y -> R y x
  R_transitive : forall x y z : D, R x y -> R y z -> R x z
  x : D
  x_Rlinked : exists y : D, R x y
  ============================
   R x x


refl_if < intro y.
Toplevel input, characters 0-7
> intro y.
> ^^^^^^^
User error: No product even after head-reduction


refl_if < 
]]


]
[#
 # Local Variables:
 # coding: raw-text-unix
 # modes: (fundamental-mode blogme-mode)
 # End:
#]