File tree Expand file tree Collapse file tree 1 file changed +36
-0
lines changed
Expand file tree Collapse file tree 1 file changed +36
-0
lines changed Original file line number Diff line number Diff line change @@ -126,3 +126,39 @@ record Context where
126126%name Context ctx
127127%runElab derive "Context" [Show, Eq, ToJSON, FromJSON]
128128```
129+
130+
131+ ## Book
132+
133+ ### ` BookItem `
134+
135+ [ ` BookItem ` ] gets a little _ fun_ because it's a mutually recursive data type, so we'll have to make a forward declaration.
136+
137+ ``` idris
138+ public export
139+ data BookItem : Type
140+
141+ public export
142+ data SectionNumber : Type where
143+ MkSectionNumber : List Nat -> SectionNumber
144+
145+ public export
146+ record ChapterItem where
147+ constructor MkChapter
148+ name : String
149+ content : String
150+ number : Maybe SectionNumber
151+ sub_items : List BookItem
152+ path : Maybe Path
153+ source_path : Maybe Path
154+ parent_names : List String
155+
156+ public export
157+ data BookItem : Type where
158+ Chapter : ChapterItem -> BookItem
159+ Seperator : BookItem
160+ PartTitle : String -> BookItem
161+
162+ %runElab derive "ChapterItem" [Show, Eq, ToJSON, FromJSON]
163+ %runElab derive "BookItem" [Show, Eq, ToJSON, FromJSON]
164+ ```
You can’t perform that action at this time.
0 commit comments