Skip to content

Commit

Permalink
indrules munger argument
Browse files Browse the repository at this point in the history
It displays inductive definitions (_rules theorem)
  • Loading branch information
dwRchyngqxs committed Apr 11, 2022
1 parent fcfee12 commit fd6d046
Showing 1 changed file with 6 additions and 2 deletions.
8 changes: 6 additions & 2 deletions src/TeX/mungeTools.sml
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,7 @@ fun stringOpt pos tok =
| "def" => SOME Def
| "indrules" => SOME IndRules
| "K" => SOME TermThm
| "m" => SOME (Mathmode "")
| "merge" => SOME Merge
| "nodefsym" => SOME NoDefSym
| "nodollarparens" => SOME NoDollarParens
Expand All @@ -69,11 +70,10 @@ fun stringOpt pos tok =
| "nostile" => SOME NoTurnstile
| "of" => SOME TypeOf
| "rule" => SOME Rule
| "showtypes" => SOME (ShowTypes 1)
| "spaceddef" => SOME SpacedDef
| "stackedrule" => SOME StackedRule
| "tt" => SOME TT
| "showtypes" => SOME (ShowTypes 1)
| "m" => SOME (Mathmode "")
| ">>" => SOME (Indent (2, true))
| ">>~" => SOME (Indent (2, false))
| _ => let val (pfx,sfx) = splitl (isNotChar #"/") ss in
Expand Down Expand Up @@ -511,6 +511,10 @@ in
block_list (block INCONSISTENT 0) pr newline lines
)
end
else if OptSet.has IndRules opts then
ind_bl (
block_list (block INCONSISTENT 0) (rule_print stdtermprint) add_newline
(map (concl o SPEC_ALL) (CONJUNCTS thm)))
else if rulep then ind_bl (rule_print stdtermprint (concl thm))
else let
val base = raw_pp_theorem_as_tex overrides
Expand Down

0 comments on commit fd6d046

Please sign in to comment.