Display 'None' when there are no injective fact instances (#612)

tamarin-prover · Apr 3, 2024 · 0e1aa8f · 0e1aa8f
1 parent d694dff
commit 0e1aa8f
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/Web/Theory.hs b/src/Web/Theory.hs
@@ -876,7 +876,7 @@ rulesSnippet thy = vcat
                                 else ppWithHeader "Macros" $ 
         (prettyMacros $ theoryMacros thy)
     , ppWithHeader "Fact Symbols with Injective Instances" $
-        fsepList (text . showInjFact) injFacts
+        (if null injFacts then text "None" else fsepList (text . showInjFact) injFacts)
     , ppWithHeader "Multiset Rewriting Rules" $
         (if null(theoryMacros thy) then text empty else text "(Shown with macros application)") <-> (vsep $ map prettyRuleAC msrRules)
     , ppWithHeader "Restrictions of the Set of Traces" $
@@ -942,7 +942,7 @@ rulesDiffSnippetSide s isdiff thy = vcat
                                      else ppWithHeader "Macros" $
         (prettyMacros $ diffTheoryMacros thy)
     ,ppWithHeader "Fact Symbols with Injective Instances" $
-        fsepList (text . showInjFact) injFacts
+        (if null injFacts then text "None" else fsepList (text . showInjFact) injFacts)
     , ppWithHeader "Multiset Rewriting Rules" $
         (if null(diffTheoryMacros thy) then text empty else text "(Shown with macros application)") <-> (vsep $ map prettyRuleAC msrRules)
     , ppWithHeader "Restrictions of the Set of Traces" $