Skip to content

Commit 423e9a7

Browse files
committed
Tactics: remove notes that were breaking PDF
1 parent 481c728 commit 423e9a7

File tree

1 file changed

+5
-11
lines changed

1 file changed

+5
-11
lines changed

src/Tactics.lidr

Lines changed: 5 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -16,22 +16,16 @@ will see:
1616
- more details on how to reason by case analysis.
1717

1818
> module Tactics
19-
19+
>
2020
> import Basics
21-
22-
\todo[inline]{If we \idr{import Poly} here, the pair sugar, among other things,
23-
will start messing things up, so we just copypaste the necessary definitions for
24-
now}
25-
26-
\todo[inline]{Describe \idr{Pruviloj} and \idr{%runElab}}
27-
2821
> import Pruviloj
29-
22+
>
3023
> %access public export
31-
24+
>
3225
> %default total
33-
26+
>
3427
> %language ElabReflection
28+
>
3529

3630

3731
== The \idr{exact} Tactic

0 commit comments

Comments
 (0)