Skip to content

Commit e9d99a3

Browse files
Moogle examples is README
1 parent 05f5fe6 commit e9d99a3

File tree

1 file changed

+28
-0
lines changed

1 file changed

+28
-0
lines changed

README.md

+28
Original file line numberDiff line numberDiff line change
@@ -16,22 +16,50 @@ The following are examples of using the leansearch API. The search is triggered
1616

1717
### Query Command
1818

19+
For `leansearch`:
20+
1921
```lean
2022
#leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."
2123
```
2224

25+
For `moogle`:
26+
27+
```lean
28+
#moogle "If a natural number n is less than m, then the successor of n is less than the successor of m."
29+
```
30+
31+
2332
### Query Term
2433

34+
For `leansearch`:
35+
2536
```lean
2637
example := #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."
2738
```
2839

40+
For `moogle`:
41+
42+
```lean
43+
example := #moogle "If a natural number n is less than m, then the successor of n is less than the successor of m."
44+
```
45+
46+
2947
### Query Tactic
3048

3149
Note that only valid tactics are displayed.
3250

51+
For `leansearch`:
52+
3353
```lean
3454
example : 3 ≤ 5 := by
3555
#leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."
3656
sorry
3757
```
58+
59+
For `moogle`:
60+
61+
```lean
62+
example : 3 ≤ 5 := by
63+
#moogle "If a natural number n is less than m, then the successor of n is less than the successor of m."
64+
sorry
65+
```

0 commit comments

Comments
 (0)