2 Data used to fill template "hbugs_tutor.TPL.ml"
4 @ADDR@ tutor ip address
6 @TACTIC@ tactic to use (OCaml function, must have type
7 ProofEngineTypes.tactic)
8 @HINT@ hint to be sent to client (content of Hbugs_types.Eureka
9 type constructor, must have type Hbugs_types.hint, see
11 @HINT_TYPE@ hint type (3rd argument of Hbugs_types.Register_tutor type
12 constructor, must have type Hbugs_types.hint_type)
13 @DESCRIPTION@ human readable tutor description
15 "source" attribute corresponding OCaml source file
17 INVARIANT: XML element name below are lowercase version of @TAGS@ used in
20 TODO: hint type isn't yet well formalized
27 <tutor source="wait_tutor.ml">
28 <addr>127.0.0.1</addr>
30 <tactic>Wait.wait_tac</tactic>
31 <hint>Hbugs_types.Use_ring_Luke</hint>
32 <hint_type>Use Ring Luke</hint_type>
33 <description>WAIT FOREVER tutor</description>
37 <tutor source="ring_tutor.ml">
38 <addr>127.0.0.1</addr>
40 <tactic>Ring.ring_tac</tactic>
41 <hint>Hbugs_types.Use_ring_Luke</hint>
42 <hint_type>Use Ring Luke</hint_type>
43 <description>Ring tutor</description>
45 <tutor source="fourier_tutor.ml">
46 <addr>127.0.0.1</addr>
48 <tactic>FourierR.fourier_tac</tactic>
49 <hint>Hbugs_types.Use_fourier_Luke</hint>
50 <hint_type>Use Fourier Luke</hint_type>
51 <description>Fourier tutor</description>
53 <tutor source="reflexivity_tutor.ml">
54 <addr>127.0.0.1</addr>
56 <tactic>EqualityTactics.reflexivity_tac</tactic>
57 <hint>Hbugs_types.Use_reflexivity_Luke</hint>
58 <hint_type>Use Reflexivity Luke</hint_type>
59 <description>Reflexivity tutor</description>
61 <tutor source="symmetry_tutor.ml">
62 <addr>127.0.0.1</addr>
64 <tactic>EqualityTactics.symmetry_tac</tactic>
65 <hint>Hbugs_types.Use_symmetry_Luke</hint>
66 <hint_type>Use Symmetry Luke</hint_type>
67 <description>Symmetry tutor</description>
69 <tutor source="assumption_tutor.ml">
70 <addr>127.0.0.1</addr>
72 <tactic>VariousTactics.assumption_tac</tactic>
73 <hint>Hbugs_types.Use_assumption_Luke</hint>
74 <hint_type>Use Assumption Luke</hint_type>
75 <description>Assumption tutor</description>
77 <tutor source="contradiction_tutor.ml">
78 <addr>127.0.0.1</addr>
80 <tactic>NegationTactics.contradiction_tac</tactic>
81 <hint>Hbugs_types.Use_contradiction_Luke</hint>
82 <hint_type>Use Contradiction Luke</hint_type>
83 <description>Contradiction tutor</description>
85 <tutor source="exists_tutor.ml">
86 <addr>127.0.0.1</addr>
88 <tactic>IntroductionTactics.exists_tac</tactic>
89 <hint>Hbugs_types.Use_exists_Luke</hint>
90 <hint_type>Use Exists Luke</hint_type>
91 <description>Exists tutor</description>
93 <tutor source="split_tutor.ml">
94 <addr>127.0.0.1</addr>
96 <tactic>IntroductionTactics.split_tac</tactic>
97 <hint>Hbugs_types.Use_split_Luke</hint>
98 <hint_type>Use Split Luke</hint_type>
99 <description>Split tutor</description>
101 <tutor source="left_tutor.ml">
102 <addr>127.0.0.1</addr>
104 <tactic>IntroductionTactics.left_tac</tactic>
105 <hint>Hbugs_types.Use_left_Luke</hint>
106 <hint_type>Use Left Luke</hint_type>
107 <description>Left tutor</description>
109 <tutor source="right_tutor.ml">
110 <addr>127.0.0.1</addr>
112 <tactic>IntroductionTactics.right_tac</tactic>
113 <hint>Hbugs_types.Use_right_Luke</hint>
114 <hint_type>Use Right Luke</hint_type>
115 <description>Right tutor</description>
117 <tutor source="search_pattern_apply_tutor.ml">
119 <addr>127.0.0.1</addr>
121 <tactic>PrimitiveTactics.apply_tac</tactic>
122 <hint>Hbugs_types.Use_apply_Luke</hint>
123 <hint_type>Use Apply Luke (with argument)</hint_type>
124 <description>Search pattern apply tutor</description>