Make breakdown total by throwing exception if impossible case happens

ayberkt · Jul 10, 2017 · fae6152 · fae6152
1 parent 6a677a7
commit fae6152
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/ljt.sml b/src/ljt.sml
@@ -123,6 +123,7 @@ structure LJT = struct
                  OneInf (DisjR2, breakdown (G || [] ===> B), goal))
         end
     | breakdown (G || [] ===> C) = searchSync G C
+    | breakdown _ = raise Fail "breakdown case not supposed to happen"
 
   and searchSync G C =
     case getSome (eliminate C) (allCtxs G) of