Skip to content

Commit 86dfb97

Browse files
committed
Restore CE tests
1 parent 91743a0 commit 86dfb97

File tree

4 files changed

+144
-204
lines changed

4 files changed

+144
-204
lines changed

Optimizations/ConditionalElimination/ConditionalElimination.thy

+2
Original file line numberDiff line numberDiff line change
@@ -1019,7 +1019,9 @@ value "
10191019
(nextNode
10201020
ConditionalEliminationTest13_testSnippet2_initial {0,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})
10211021
"
1022+
(*
10221023
values "{g|g. (ConditionalEliminationPhase ({}, Map.empty) ConditionalEliminationTest13_testSnippet2_initial g)}"
1024+
*)
10231025
(*
10241026
inductive ConditionalEliminationPhaseWithTrace\<^marker>\<open>tag invisible\<close>
10251027
:: "IRGraph \<Rightarrow> (ID \<times> Seen \<times> Conditions \<times> StampFlow) \<Rightarrow> ID list \<Rightarrow> IRGraph \<Rightarrow> ID list \<Rightarrow> Conditions \<Rightarrow> bool" where\<^marker>\<open>tag invisible\<close>

ROOT

+3-1
Original file line numberDiff line numberDiff line change
@@ -101,9 +101,11 @@ session ConditionalElimination in "Optimizations/ConditionalElimination" = Proof
101101
"(experimental) Conditional elimination phase"
102102
options [quick_and_dirty,
103103
document = pdf, document_output = "output",
104-
show_question_marks = false]
104+
show_question_marks = false,
105+
document_variants="document:outline=/proof"]
105106
theories
106107
ConditionalElimination
108+
CFG
107109
document_files (in "../../latex")
108110
"root.tex"
109111
"mathpartir.sty"

0 commit comments

Comments
 (0)