package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/src/rocq-runtime.toplevel/g_toplevel.ml.html
Source file g_toplevel.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137
# 13 "toplevel/g_toplevel.mlg" open Procq open Procq.Prim open Vernacexpr (* Vernaculars specific to the toplevel *) type vernac_toplevel = | VernacBackTo of int | VernacDrop | VernacQuit | VernacControl of vernac_control | VernacShowGoal of { gid : int; sid: int } | VernacShowProofDiffs of Proof_diffs.diffOpt let vernac_toplevel = Entry.make "toplevel:vernac_toplevel" let err () = raise Gramlib.Stream.Failure let test_show_goal = let open Procq.Lookahead in to_entry "test_show_goal" begin lk_kw "Show" >> lk_kw "Goal" >> lk_nat end let _ = let () = Procq.grammar_extend vernac_toplevel (Procq.Fresh (Gramlib.Gramext.First, [(None, None, [Procq.Production.make (Procq.Rule.next (Procq.Rule.stop) ((Procq.Symbol.nterm Pvernac.Vernac_.main_entry))) (fun cmd loc -> # 53 "toplevel/g_toplevel.mlg" match cmd with | None -> None | Some v -> Some (VernacControl v) ); Procq.Production.make (Procq.Rule.next (Procq.Rule.next (Procq.Rule.next (Procq.Rule.next (Procq.Rule.next (Procq.Rule.stop) ((Procq.Symbol.token (Tok.PIDENT (Some ("Show")))))) ((Procq.Symbol.token (Tok.PIDENT (Some ("Proof")))))) ((Procq.Symbol.token (Tok.PIDENT (Some ("Diffs")))))) ((Procq.Symbol.opt (Procq.Symbol.rules [Procq.Rules.make ( Procq.Rule.next_norec (Procq.Rule.stop) ((Procq.Symbol.token (Tok.PIDENT (Some ("removed")))))) (fun _ loc -> # 49 "toplevel/g_toplevel.mlg" () )])))) ((Procq.Symbol.token (Tok.PKEYWORD ("."))))) (fun _ removed _ _ _ loc -> # 50 "toplevel/g_toplevel.mlg" Some (VernacShowProofDiffs (if removed = None then Proof_diffs.DiffOn else Proof_diffs.DiffRemoved)) ); Procq.Production.make (Procq.Rule.next (Procq.Rule.next (Procq.Rule.next (Procq.Rule.next (Procq.Rule.next (Procq.Rule.next (Procq.Rule.next (Procq.Rule.stop) ((Procq.Symbol.nterm test_show_goal))) ((Procq.Symbol.token (Tok.PIDENT (Some ("Show")))))) ((Procq.Symbol.token (Tok.PIDENT (Some ("Goal")))))) ((Procq.Symbol.nterm natural))) ((Procq.Symbol.token (Tok.PIDENT (Some ("at")))))) ((Procq.Symbol.nterm natural))) ((Procq.Symbol.token (Tok.PKEYWORD ("."))))) (fun _ sid _ gid _ _ _ loc -> # 48 "toplevel/g_toplevel.mlg" Some (VernacShowGoal {gid; sid}) ); Procq.Production.make (Procq.Rule.next (Procq.Rule.next (Procq.Rule.next (Procq.Rule.stop) ((Procq.Symbol.token (Tok.PIDENT (Some ("BackTo")))))) ((Procq.Symbol.nterm natural))) ((Procq.Symbol.token (Tok.PKEYWORD ("."))))) (fun _ n _ loc -> # 45 "toplevel/g_toplevel.mlg" Some (VernacBackTo n) ); Procq.Production.make (Procq.Rule.next (Procq.Rule.next (Procq.Rule.stop) ((Procq.Symbol.token (Tok.PIDENT (Some ("Quit")))))) ((Procq.Symbol.token (Tok.PKEYWORD ("."))))) (fun _ _ loc -> # 43 "toplevel/g_toplevel.mlg" Some VernacQuit ); Procq.Production.make (Procq.Rule.next (Procq.Rule.next (Procq.Rule.stop) ((Procq.Symbol.token (Tok.PIDENT (Some ("Drop")))))) ((Procq.Symbol.token (Tok.PKEYWORD ("."))))) (fun _ _ loc -> # 42 "toplevel/g_toplevel.mlg" Some VernacDrop )])])) in () # 61 "toplevel/g_toplevel.mlg" let vernac_toplevel pm = Pvernac.Unsafe.set_tactic_entry pm; vernac_toplevel
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>