structural-induction 0.1.1 → 0.1.2

raw patch · 3 files changed

+5/−3 lines, 3 files

Files

• Induction/Structural/Types.hs +2/−0
• structural-induction.cabal +2/−2
• test/Main.hs +1/−1

@@ -148,6 +148,8 @@ -- | Obligations with tagged variables (see `Tagged` and `unTag`) type TaggedObligation c v t = Obligation c (Tagged v) t +return []+ -- | Tri-traverse of Obligation trObligation :: Applicative f => (c -> f c') -> (v -> f v') -> (t -> f t') -> Obligation c v t -> f (Obligation c' v' t') trObligation = $(genTraverse ''Obligation)

@@ -1,6 +1,6 @@ name:               structural-induction category:           Theorem Provers, Logic-version:            0.1.1+version:            0.1.2 license:            LGPL-3 license-file:       LICENSE author:             Dan Rosén@@ -9,7 +9,7 @@ bug-reports:        http://www.github.com/danr/structural-induction/issues build-type:         Simple cabal-version:      >= 1.8-tested-with:        GHC == 7.4.1, GHC == 7.6.1+tested-with:        GHC == 7.4.2, GHC == 7.6.3, GHC == 7.8.3 synopsis:           Instantiate structural induction schemas for algebraic data types description:        See documentation for Induction.Structural 

@@ -91,7 +91,7 @@     forAllShrink (startFromTypes tys) (mapM shrinkRepr') $ \ start ->         forAll (makeTracer start parts) $ \ trace ->             case loop trace of-                Just _  -> printTestCase (showOblig parts) False+                Just _  -> counterexample (showOblig parts) False                 Nothing -> property True   where parts = ind sii tc