-- we can read Lua syntax here!
return {
    ["bbox"] = {
        [1] = {
            ["x0"] = 44,
            ["x1"] = 395,
            ["y0"] = 65,
            ["y1"] = 646,
        },
        [2] = {
            ["x0"] = 38,
            ["x1"] = 406,
            ["y0"] = 27,
            ["y1"] = 656,
        },
        [3] = {
            ["x0"] = 32,
            ["x1"] = 404,
            ["y0"] = 25,
            ["y1"] = 655,
        },
        ["even"] = {
            ["x0"] = 38,
            ["x1"] = 406,
            ["y0"] = 27,
            ["y1"] = 656,
        },
        ["odd"] = {
            ["x0"] = 32,
            ["x1"] = 404,
            ["y0"] = 25,
            ["y1"] = 655,
        },
    },
    ["bookmarks"] = {
        [1] = {
            ["chapter"] = "2.2 Related Automation Techniques",
            ["datetime"] = "2023-04-15 19:35:04",
            ["highlighted"] = true,
            ["notes"] = "The encodings of the logics of proof assistants based on the Calculus of Constructions and its extensions in first-order logic have so far covered only very limited fragments of the source logic [2,16,69]. Why3 [35] provides a translation from its own logic [33] (which is a subset of the Coq logic, including features like rank-1 polymorphism, algebraic data types, recursive functions and inductive predicates)",
            ["page"] = 4,
            ["pos0"] = {
                ["page"] = 4,
                ["x"] = 54.540740740741,
                ["y"] = 450.66851851852,
            },
            ["pos1"] = {
                ["page"] = 4,
                ["x"] = 156.2287037037,
                ["y"] = 496.53148148148,
            },
            ["text"] = "Page 4 The encodings of the logics of proof assistants based on the Calculus of Constructions and its extensions in first-order logic have so far covered only very limited fragments of the source logic [2,16,69]. Why3 [35] provides a translation from its own logic [33] (which is a subset of the Coq logic, including features like rank-1 polymorphism, algebraic data types, recursive functions and inductive predicates) @ 2023-04-15 19:35:04",
        },
    },
    ["bookmarks_sorted"] = true,
    ["bookmarks_sorted_20220106"] = true,
    ["bookmarks_version"] = 20200615,
    ["config_panel_index"] = 2,
    ["disable_fuzzy_search"] = false,
    ["doc_pages"] = 31,
    ["doc_path"] = "/mnt/onboard/Czajka, Lukasz & Kaliszyk, Cezary/Hammer for Coq_ Automation for Dependent Type Theory - Lukasz Czajka & Cezary Kaliszyk.pdf",
    ["doc_props"] = {
        ["author"] = "Łukasz Czajka & Cezary Kaliszyk",
        ["authors"] = "Łukasz Czajka & Cezary Kaliszyk",
        ["creationDate"] = "D:20180226135720+05'30'",
        ["creator"] = "Springer",
        ["description"] = "Journal of Automated Reasoning, https://doi.org/10.1007/s10817-018-9458-4",
        ["keywords"] = "nonfiction, thesis",
        ["language"] = "",
        ["modDate"] = "D:20230407234318+02'00'",
        ["producer"] = "Acrobat Distiller 10.1.8 (Windows)",
        ["series"] = "",
        ["subject"] = "Journal of Automated Reasoning, https://doi.org/10.1007/s10817-018-9458-4",
        ["title"] = "Hammer for Coq: Automation for Dependent Type Theory",
    },
    ["flipping_scroll_mode"] = true,
    ["flipping_zoom_mode"] = "page",
    ["gamma"] = 1,
    ["highlight"] = {
        [4] = {
            [1] = {
                ["chapter"] = "2.2 Related Automation Techniques",
                ["datetime"] = "2023-04-15 19:35:04",
                ["drawer"] = "lighten",
                ["pboxes"] = {
                    [1] = {
                        ["h"] = 10.562377929688,
                        ["w"] = 345.82624816895,
                        ["x"] = 47.195999145508,
                        ["y"] = 444.15682983398,
                    },
                    [2] = {
                        ["h"] = 10.562377929688,
                        ["w"] = 345.85554504395,
                        ["x"] = 47.195999145508,
                        ["y"] = 455.61358642578,
                    },
                    [3] = {
                        ["h"] = 10.562377929688,
                        ["w"] = 345.82905578613,
                        ["x"] = 47.195999145508,
                        ["y"] = 467.07034301758,
                    },
                    [4] = {
                        ["h"] = 10.562377929688,
                        ["w"] = 345.83374023438,
                        ["x"] = 47.196960449219,
                        ["y"] = 478.52713012695,
                    },
                    [5] = {
                        ["h"] = 10.562377929688,
                        ["w"] = 131.52723693848,
                        ["x"] = 47.196960449219,
                        ["y"] = 489.98391723633,
                    },
                },
                ["pos0"] = {
                    ["page"] = 4,
                    ["x"] = 54.540740740741,
                    ["y"] = 450.66851851852,
                },
                ["pos1"] = {
                    ["page"] = 4,
                    ["x"] = 156.2287037037,
                    ["y"] = 496.53148148148,
                },
                ["text"] = "The encodings of the logics of proof assistants based on the Calculus of Constructions and its extensions in first-order logic have so far covered only very limited fragments of the source logic [2,16,69]. Why3 [35] provides a translation from its own logic [33] (which is a subset of the Coq logic, including features like rank-1 polymorphism, algebraic data types, recursive functions and inductive predicates)",
            },
        },
    },
    ["highlight_drawer"] = "lighten",
    ["highlights_imported"] = true,
    ["inverse_reading_order"] = false,
    ["kopt_auto_straighten"] = 0,
    ["kopt_contrast"] = 1,
    ["kopt_defect_size"] = 1,
    ["kopt_detect_indent"] = 1,
    ["kopt_doc_language"] = "eng",
    ["kopt_font_fine_tune"] = 0.05,
    ["kopt_font_size"] = 1,
    ["kopt_forced_ocr"] = 0,
    ["kopt_full_screen"] = 1,
    ["kopt_hw_dithering"] = 0,
    ["kopt_justification"] = 3,
    ["kopt_line_spacing"] = 1.2,
    ["kopt_max_columns"] = 1,
    ["kopt_page_gap_height"] = 8,
    ["kopt_page_margin"] = 0.4,
    ["kopt_page_opt"] = 0,
    ["kopt_page_scroll"] = 1,
    ["kopt_quality"] = 1,
    ["kopt_rotation_mode"] = 0,
    ["kopt_sw_dithering"] = 0,
    ["kopt_text_wrap"] = 1,
    ["kopt_trim_page"] = 2,
    ["kopt_word_spacing"] = -0.2,
    ["kopt_writing_direction"] = 0,
    ["kopt_zoom_direction"] = 7,
    ["kopt_zoom_factor"] = 1.5,
    ["kopt_zoom_mode_genus"] = 4,
    ["kopt_zoom_mode_type"] = 2,
    ["kopt_zoom_overlap_h"] = 36,
    ["kopt_zoom_overlap_v"] = 36,
    ["kopt_zoom_range_number"] = 2,
    ["last_page"] = 4,
    ["normal_zoom_mode"] = "page",
    ["page_overlap_style"] = "dim",
    ["page_positions"] = {
        [-9] = 0,
        [-3] = 0,
        [1] = 0.52849291293029,
        [2] = 0,
        [3] = 0.74460499155564,
        [4] = 0.79166666666667,
        [5] = 0.79321769635549,
        [6] = 0.143815915628,
        [7] = 0,
        [17] = 0,
        [18] = 0,
        [21] = 0,
        [23] = 0.90341578327444,
        [24] = 0.29993577392421,
        [25] = 0.074918566775245,
        [26] = 0.18842062193126,
        [27] = 0.292578125,
        [28] = 0.0030763314747168,
        [29] = 0.34529803475719,
    },
    ["panel_zoom_enabled"] = false,
    ["partial_md5_checksum"] = "d41e953353a8c735ab6e770580c67572",
    ["percent_finished"] = 0.16129032258065,
    ["preferred_dictionaries"] = {},
    ["readermenu_tab_index"] = 1,
    ["render_mode"] = 0,
    ["rotation_mode"] = 0,
    ["show_overlap_enable"] = false,
    ["stats"] = {
        ["authors"] = "Łukasz Czajka & Cezary Kaliszyk",
        ["highlights"] = 1,
        ["language"] = "N/A",
        ["md5"] = "d41e953353a8c735ab6e770580c67572",
        ["notes"] = 0,
        ["pages"] = 31,
        ["series"] = "N/A",
        ["title"] = "Hammer for Coq: Automation for Dependent Type Theory",
    },
    ["summary"] = {
        ["modified"] = "2023-04-14",
        ["status"] = "reading",
    },
    ["tile_cache_validity_ts"] = 1681601121,
    ["toc_ticks_ignored_levels"] = {},
    ["zoom_mode"] = "page",
    ["zoom_overlap_h"] = 40,
    ["zoom_overlap_v"] = 40,
}
