Hi Lukas, I am currently stuck with a problem in Quickcheck/Narrowing.
After about 10 years it came to surface that code generation for Haskell may produce irrefutable patterns due to pattern bindings in let clauses. See <https://wiki.haskell.org/Lazy_pattern_match>; if I understand <https://www.haskell.org/tutorial/patterns.html> correctly that particular semantics allows fancy definitions like the following fibonacci one-liner: »fib @ (1 : more_fib) = 1 : 1 : [ a + b | (a, b) <- zip fib more_fib ]«. However the partial correctness approach of the code generator assumes that pattern match clauses may silently be dropped, which is made use of to translate the HOL-ish »partial« undefined conveniently. This breaks down in presence of irrefutable patterns (see the post on isabelle-users by Rene Thiemann). The correction is obvious: for Haskell, only local variables may be bound by let clauses, but never patterns – these are solely bound by case clauses, which are strict in Haskell (as in function equations). This however breaks Quickcheck/Narrowing where the lazy nature of pattern bindings has been exploited, may be unconsciously. A minimal example is attached (Quickcheck_Narrowing_Examples.thy) but I also distilled the generated Haskell code: The same before and after: Typerep.hs Then the difference occurs: Generated_Code.hs Before: Generated_Code.A.hs After: Generated_Code.B.hs The same before and after: Narrowing_Engine.hs Main.hs The diff ist straight-forward to read: > 93,102c93,106 > < let { > < (Narrowing_cons (Narrowing_sum_of_products ps) cfs) = f d; > < (Narrowing_cons ta cas) = a (d - (1 :: Prelude.Int)); > < shallow = (0 :: Prelude.Int) < d && non_empty ta; > < aa = (if shallow then map (\ cf (x : xs) -> cf xs (conv cas x)) > cfs > < else []); > < } in Narrowing_cons > < (Narrowing_sum_of_products > < (if shallow then map (\ ab -> ta : ab) ps else [])) > < aa; > --- > > (case f d of { > > Narrowing_cons (Narrowing_sum_of_products ps) cfs -> > > (case a (d - (1 :: Prelude.Int)) of { > > Narrowing_cons ta cas -> > > let { > > shallow = (0 :: Prelude.Int) < d && non_empty ta; > > aa = (if shallow then map (\ cf (x : xs) -> cf xs (conv > cas x)) cfs > > else []); > > } in Narrowing_cons > > (Narrowing_sum_of_products > > (if shallow then map (\ ab -> ta : ab) ps else [])) > > aa; > > }); > > }); > 112,115c116,122 > < let { > < (Narrowing_cons (Narrowing_sum_of_products ssa) ca) = a d; > < (Narrowing_cons (Narrowing_sum_of_products ssb) cb) = b d; > < } in Narrowing_cons (Narrowing_sum_of_products (ssa ++ ssb)) (ca ++ > cb); > --- > > (case a d of { > > Narrowing_cons (Narrowing_sum_of_products ssa) ca -> > > (case b d of { > > Narrowing_cons (Narrowing_sum_of_products ssb) cb -> > > Narrowing_cons (Narrowing_sum_of_products (ssa ++ ssb)) (ca > ++ cb); > > }); > > }); Unfortunately my knowledge is too restricted what could be done here to restore the intended behaviour economically. Hence I ask whether you have an idea what is going wrong here. Thanks a lot! Florian -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
Quickcheck_Narrowing_Examples.thy
Description: application/extension-thy
module
Generated_Code(Narrowing_type(..), Narrowing_term(..), Term(..), Itself(..),
Typerepa(..), Partial_term_of(..), Is_testable(..),
Narrowing_cons(..), Narrowing(..), Term_of(..), Num(..),
Char(..), Nat(..), typerep_nat, term_of_nat, non_empty, conv,
apply, cons, sum, narrowing_nat, partial_term_of_nat,
typerep_bool, narrowing_bool, partial_term_of_bool,
narrowing_dummy_partial_term_of, narrowing_dummy_narrowing,
ensure_testable, equal_nat, value)
where {
import Prelude ((==), (/=), (<), (<=), (>=), (>), (+), (-), (*), (/), (**),
(>>=), (>>), (=<<), (&&), (||), (^), (^^), (.), ($), ($!), (++), (!!), Eq,
error, id, return, not, fst, snd, map, filter, concat, concatMap, reverse,
zip, null, takeWhile, dropWhile, all, any, Integer, negate, abs, divMod,
String, Bool(True, False), Maybe(Nothing, Just));
import qualified Prelude;
import qualified Typerep;
newtype Narrowing_type = Narrowing_sum_of_products [[Narrowing_type]];
data Narrowing_term = Narrowing_variable [Prelude.Int] Narrowing_type
| Narrowing_constructor Prelude.Int [Narrowing_term];
data Term = Const String Typerep.Typerep | App Term Term
| Abs String Typerep.Typerep Term | Free String Typerep.Typerep;
data Itself a = Type;
class Typerepa a where {
typerep :: Itself a -> Typerep.Typerep;
};
class (Typerepa a) => Partial_term_of a where {
partial_term_of :: Itself a -> Narrowing_term -> Term;
};
class Is_testable a where {
};
data Narrowing_cons a = Narrowing_cons Narrowing_type [[Narrowing_term] -> a];
class Narrowing a where {
narrowing :: Prelude.Int -> Narrowing_cons a;
};
class (Typerepa a) => Term_of a where {
term_of :: a -> Term;
};
instance (Term_of a, Narrowing a, Partial_term_of a,
Is_testable b) => Is_testable (a -> b) where {
};
data Num = One | Bit0 Num | Bit1 Num;
data Char = Zero_char | Char Num;
data Nat = Zero_nat | Suc Nat;
typerep_nat :: Itself Nat -> Typerep.Typerep;
typerep_nat t = Typerep.Typerep "Nat.nat" [];
instance Typerepa Nat where {
typerep = typerep_nat;
};
term_of_nat :: Nat -> Term;
term_of_nat (Suc a) =
App (Const "Nat.Suc"
(Typerep.Typerep "fun"
[Typerep.Typerep "Nat.nat" [], Typerep.Typerep "Nat.nat" []]))
(term_of_nat a);
term_of_nat Zero_nat =
Const "Nat.zero_nat_inst.zero_nat" (Typerep.Typerep "Nat.nat" []);
instance Term_of Nat where {
term_of = term_of_nat;
};
non_empty :: Narrowing_type -> Bool;
non_empty (Narrowing_sum_of_products ps) = not (null ps);
conv :: forall a. [[Narrowing_term] -> a] -> Narrowing_term -> a;
conv cs (Narrowing_variable p uu) = error ('\0' : map Prelude.toEnum p);
conv cs (Narrowing_constructor i xs) = (cs !! i) xs;
apply ::
forall a b.
(Prelude.Int -> Narrowing_cons (a -> b)) ->
(Prelude.Int -> Narrowing_cons a) -> Prelude.Int -> Narrowing_cons b;
apply f a d =
let {
(Narrowing_cons (Narrowing_sum_of_products ps) cfs) = f d;
(Narrowing_cons ta cas) = a (d - (1 :: Prelude.Int));
shallow = (0 :: Prelude.Int) < d && non_empty ta;
aa = (if shallow then map (\ cf (x : xs) -> cf xs (conv cas x)) cfs
else []);
} in Narrowing_cons
(Narrowing_sum_of_products
(if shallow then map (\ ab -> ta : ab) ps else []))
aa;
cons :: forall a. a -> Prelude.Int -> Narrowing_cons a;
cons a d = Narrowing_cons (Narrowing_sum_of_products [[]]) [(\ _ -> a)];
sum ::
forall a.
(Prelude.Int -> Narrowing_cons a) ->
(Prelude.Int -> Narrowing_cons a) -> Prelude.Int -> Narrowing_cons a;
sum a b d =
let {
(Narrowing_cons (Narrowing_sum_of_products ssa) ca) = a d;
(Narrowing_cons (Narrowing_sum_of_products ssb) cb) = b d;
} in Narrowing_cons (Narrowing_sum_of_products (ssa ++ ssb)) (ca ++ cb);
narrowing_nat :: Prelude.Int -> Narrowing_cons Nat;
narrowing_nat = sum (cons Zero_nat) (apply (cons Suc) narrowing_nat);
instance Narrowing Nat where {
narrowing = narrowing_nat;
};
partial_term_of_nat :: Itself Nat -> Narrowing_term -> Term;
partial_term_of_nat ty (Narrowing_constructor (1 :: Prelude.Int) [a]) =
App (Const "Nat.Suc"
(Typerep.Typerep "fun"
[Typerep.Typerep "Nat.nat" [], Typerep.Typerep "Nat.nat" []]))
(partial_term_of_nat Type a);
partial_term_of_nat ty (Narrowing_constructor (0 :: Prelude.Int) []) =
Const "Nat.zero_nat_inst.zero_nat" (Typerep.Typerep "Nat.nat" []);
partial_term_of_nat ty (Narrowing_variable p tt) =
Free "_" (Typerep.Typerep "Nat.nat" []);
instance Partial_term_of Nat where {
partial_term_of = partial_term_of_nat;
};
typerep_bool :: Itself Bool -> Typerep.Typerep;
typerep_bool t = Typerep.Typerep "HOL.bool" [];
instance Typerepa Bool where {
typerep = typerep_bool;
};
narrowing_bool :: Prelude.Int -> Narrowing_cons Bool;
narrowing_bool = sum (cons True) (cons False);
instance Narrowing Bool where {
narrowing = narrowing_bool;
};
instance Is_testable Bool where {
};
partial_term_of_bool :: Itself Bool -> Narrowing_term -> Term;
partial_term_of_bool ty (Narrowing_constructor (1 :: Prelude.Int) []) =
Const "HOL.False" (Typerep.Typerep "HOL.bool" []);
partial_term_of_bool ty (Narrowing_constructor (0 :: Prelude.Int) []) =
Const "HOL.True" (Typerep.Typerep "HOL.bool" []);
partial_term_of_bool ty (Narrowing_variable p tt) =
Free "_" (Typerep.Typerep "HOL.bool" []);
instance Partial_term_of Bool where {
partial_term_of = partial_term_of_bool;
};
narrowing_dummy_partial_term_of ::
forall a. (Partial_term_of a) => Itself a -> Narrowing_term -> Term;
narrowing_dummy_partial_term_of = partial_term_of;
narrowing_dummy_narrowing ::
forall a. (Narrowing a) => Prelude.Int -> Narrowing_cons a;
narrowing_dummy_narrowing = narrowing;
ensure_testable :: forall a. (Is_testable a) => a -> a;
ensure_testable f =
let {
_ = (narrowing_dummy_narrowing :: Prelude.Int -> Narrowing_cons Bool);
_ = (narrowing_dummy_partial_term_of ::
Itself Bool -> Narrowing_term -> Term);
_ = conv;
} in f;
equal_nat :: Nat -> Nat -> Bool;
equal_nat Zero_nat (Suc x2) = False;
equal_nat (Suc x2) Zero_nat = False;
equal_nat (Suc x2) (Suc y2) = equal_nat x2 y2;
equal_nat Zero_nat Zero_nat = True;
value :: forall a. a -> Nat -> Nat -> Bool;
value dummy = ensure_testable (\ y x -> equal_nat x y);
}
module
Generated_Code(Narrowing_type(..), Narrowing_term(..), Term(..), Itself(..),
Typerepa(..), Partial_term_of(..), Is_testable(..),
Narrowing_cons(..), Narrowing(..), Term_of(..), Num(..),
Char(..), Nat(..), typerep_nat, term_of_nat, non_empty, conv,
apply, cons, sum, narrowing_nat, partial_term_of_nat,
typerep_bool, narrowing_bool, partial_term_of_bool,
narrowing_dummy_partial_term_of, narrowing_dummy_narrowing,
ensure_testable, equal_nat, value)
where {
import Prelude ((==), (/=), (<), (<=), (>=), (>), (+), (-), (*), (/), (**),
(>>=), (>>), (=<<), (&&), (||), (^), (^^), (.), ($), ($!), (++), (!!), Eq,
error, id, return, not, fst, snd, map, filter, concat, concatMap, reverse,
zip, null, takeWhile, dropWhile, all, any, Integer, negate, abs, divMod,
String, Bool(True, False), Maybe(Nothing, Just));
import qualified Prelude;
import qualified Typerep;
newtype Narrowing_type = Narrowing_sum_of_products [[Narrowing_type]];
data Narrowing_term = Narrowing_variable [Prelude.Int] Narrowing_type
| Narrowing_constructor Prelude.Int [Narrowing_term];
data Term = Const String Typerep.Typerep | App Term Term
| Abs String Typerep.Typerep Term | Free String Typerep.Typerep;
data Itself a = Type;
class Typerepa a where {
typerep :: Itself a -> Typerep.Typerep;
};
class (Typerepa a) => Partial_term_of a where {
partial_term_of :: Itself a -> Narrowing_term -> Term;
};
class Is_testable a where {
};
data Narrowing_cons a = Narrowing_cons Narrowing_type [[Narrowing_term] -> a];
class Narrowing a where {
narrowing :: Prelude.Int -> Narrowing_cons a;
};
class (Typerepa a) => Term_of a where {
term_of :: a -> Term;
};
instance (Term_of a, Narrowing a, Partial_term_of a,
Is_testable b) => Is_testable (a -> b) where {
};
data Num = One | Bit0 Num | Bit1 Num;
data Char = Zero_char | Char Num;
data Nat = Zero_nat | Suc Nat;
typerep_nat :: Itself Nat -> Typerep.Typerep;
typerep_nat t = Typerep.Typerep "Nat.nat" [];
instance Typerepa Nat where {
typerep = typerep_nat;
};
term_of_nat :: Nat -> Term;
term_of_nat (Suc a) =
App (Const "Nat.Suc"
(Typerep.Typerep "fun"
[Typerep.Typerep "Nat.nat" [], Typerep.Typerep "Nat.nat" []]))
(term_of_nat a);
term_of_nat Zero_nat =
Const "Nat.zero_nat_inst.zero_nat" (Typerep.Typerep "Nat.nat" []);
instance Term_of Nat where {
term_of = term_of_nat;
};
non_empty :: Narrowing_type -> Bool;
non_empty (Narrowing_sum_of_products ps) = not (null ps);
conv :: forall a. [[Narrowing_term] -> a] -> Narrowing_term -> a;
conv cs (Narrowing_variable p uu) = error ('\0' : map Prelude.toEnum p);
conv cs (Narrowing_constructor i xs) = (cs !! i) xs;
apply ::
forall a b.
(Prelude.Int -> Narrowing_cons (a -> b)) ->
(Prelude.Int -> Narrowing_cons a) -> Prelude.Int -> Narrowing_cons b;
apply f a d =
(case f d of {
Narrowing_cons (Narrowing_sum_of_products ps) cfs ->
(case a (d - (1 :: Prelude.Int)) of {
Narrowing_cons ta cas ->
let {
shallow = (0 :: Prelude.Int) < d && non_empty ta;
aa = (if shallow then map (\ cf (x : xs) -> cf xs (conv cas x)) cfs
else []);
} in Narrowing_cons
(Narrowing_sum_of_products
(if shallow then map (\ ab -> ta : ab) ps else []))
aa;
});
});
cons :: forall a. a -> Prelude.Int -> Narrowing_cons a;
cons a d = Narrowing_cons (Narrowing_sum_of_products [[]]) [(\ _ -> a)];
sum ::
forall a.
(Prelude.Int -> Narrowing_cons a) ->
(Prelude.Int -> Narrowing_cons a) -> Prelude.Int -> Narrowing_cons a;
sum a b d =
(case a d of {
Narrowing_cons (Narrowing_sum_of_products ssa) ca ->
(case b d of {
Narrowing_cons (Narrowing_sum_of_products ssb) cb ->
Narrowing_cons (Narrowing_sum_of_products (ssa ++ ssb)) (ca ++ cb);
});
});
narrowing_nat :: Prelude.Int -> Narrowing_cons Nat;
narrowing_nat = sum (cons Zero_nat) (apply (cons Suc) narrowing_nat);
instance Narrowing Nat where {
narrowing = narrowing_nat;
};
partial_term_of_nat :: Itself Nat -> Narrowing_term -> Term;
partial_term_of_nat ty (Narrowing_constructor (1 :: Prelude.Int) [a]) =
App (Const "Nat.Suc"
(Typerep.Typerep "fun"
[Typerep.Typerep "Nat.nat" [], Typerep.Typerep "Nat.nat" []]))
(partial_term_of_nat Type a);
partial_term_of_nat ty (Narrowing_constructor (0 :: Prelude.Int) []) =
Const "Nat.zero_nat_inst.zero_nat" (Typerep.Typerep "Nat.nat" []);
partial_term_of_nat ty (Narrowing_variable p tt) =
Free "_" (Typerep.Typerep "Nat.nat" []);
instance Partial_term_of Nat where {
partial_term_of = partial_term_of_nat;
};
typerep_bool :: Itself Bool -> Typerep.Typerep;
typerep_bool t = Typerep.Typerep "HOL.bool" [];
instance Typerepa Bool where {
typerep = typerep_bool;
};
narrowing_bool :: Prelude.Int -> Narrowing_cons Bool;
narrowing_bool = sum (cons True) (cons False);
instance Narrowing Bool where {
narrowing = narrowing_bool;
};
instance Is_testable Bool where {
};
partial_term_of_bool :: Itself Bool -> Narrowing_term -> Term;
partial_term_of_bool ty (Narrowing_constructor (1 :: Prelude.Int) []) =
Const "HOL.False" (Typerep.Typerep "HOL.bool" []);
partial_term_of_bool ty (Narrowing_constructor (0 :: Prelude.Int) []) =
Const "HOL.True" (Typerep.Typerep "HOL.bool" []);
partial_term_of_bool ty (Narrowing_variable p tt) =
Free "_" (Typerep.Typerep "HOL.bool" []);
instance Partial_term_of Bool where {
partial_term_of = partial_term_of_bool;
};
narrowing_dummy_partial_term_of ::
forall a. (Partial_term_of a) => Itself a -> Narrowing_term -> Term;
narrowing_dummy_partial_term_of = partial_term_of;
narrowing_dummy_narrowing ::
forall a. (Narrowing a) => Prelude.Int -> Narrowing_cons a;
narrowing_dummy_narrowing = narrowing;
ensure_testable :: forall a. (Is_testable a) => a -> a;
ensure_testable f =
let {
_ = (narrowing_dummy_narrowing :: Prelude.Int -> Narrowing_cons Bool);
_ = (narrowing_dummy_partial_term_of ::
Itself Bool -> Narrowing_term -> Term);
_ = conv;
} in f;
equal_nat :: Nat -> Nat -> Bool;
equal_nat Zero_nat (Suc x2) = False;
equal_nat (Suc x2) Zero_nat = False;
equal_nat (Suc x2) (Suc y2) = equal_nat x2 y2;
equal_nat Zero_nat Zero_nat = True;
value :: forall a. a -> Nat -> Nat -> Bool;
value dummy = ensure_testable (\ y x -> equal_nat x y);
}
module Main where {
import System.IO;
import System.Environment;
import Narrowing_Engine;
import Generated_Code ;
main = getArgs >>= \[potential, size] -> Narrowing_Engine.depthCheck (read potential) (read size) (Generated_Code.value ())
}
module Narrowing_Engine where {
import Control.Monad;
import Control.Exception;
import System.IO;
import System.Exit;
import qualified Typerep;
import qualified Generated_Code;
type Pos = [Int];
-- Term refinement
new :: Pos -> [[Generated_Code.Narrowing_type]] -> [Generated_Code.Narrowing_term];
new p ps = [ Generated_Code.Narrowing_constructor c (zipWith (\i t -> Generated_Code.Narrowing_variable (p++[i]) t) [0..] ts)
| (c, ts) <- zip [0..] ps ];
refine :: Generated_Code.Narrowing_term -> Pos -> [Generated_Code.Narrowing_term];
refine (Generated_Code.Narrowing_variable p (Generated_Code.Narrowing_sum_of_products ss)) [] = new p ss;
refine (Generated_Code.Narrowing_constructor c xs) p = map (Generated_Code.Narrowing_constructor c) (refineList xs p);
refineList :: [Generated_Code.Narrowing_term] -> Pos -> [[Generated_Code.Narrowing_term]];
refineList xs (i:is) = let (ls, x:rs) = splitAt i xs in [ls ++ y:rs | y <- refine x is];
-- Find total instantiations of a partial value
total :: Generated_Code.Narrowing_term -> [Generated_Code.Narrowing_term];
total (Generated_Code.Narrowing_constructor c xs) = [Generated_Code.Narrowing_constructor c ys | ys <- mapM total xs];
total (Generated_Code.Narrowing_variable p (Generated_Code.Narrowing_sum_of_products ss)) = [y | x <- new p ss, y <- total x];
-- Answers
answeri :: a -> (Bool -> a -> IO b) -> (Pos -> IO b) -> IO b;
answeri a known unknown =
try (evaluate a) >>= (\res ->
case res of
Right b -> known True b
Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
Left e -> throw e);
answer :: Bool -> Bool -> (Bool -> Bool -> IO b) -> (Pos -> IO b) -> IO b;
answer genuine_only a known unknown =
Control.Exception.catch (answeri a known unknown)
(\ (PatternMatchFail _) -> known False genuine_only);
-- Refute
str_of_list [] = "[]";
str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")";
report :: Bool -> Result -> [Generated_Code.Narrowing_term] -> IO Int;
report genuine r xs = putStrLn ("SOME (" ++ (if genuine then "true" else "false") ++
", " ++ (str_of_list $ zipWith ($) (showArgs r) xs) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
eval :: Bool -> Bool -> (Bool -> Bool -> IO a) -> (Pos -> IO a) -> IO a;
eval genuine_only p k u = answer genuine_only p k u;
ref :: Bool -> Result -> [Generated_Code.Narrowing_term] -> IO Int;
ref genuine_only r xs = eval genuine_only (apply_fun r xs) (\genuine res -> if res then return 1 else report genuine r xs)
(\p -> sumMapM (ref genuine_only r) 1 (refineList xs p));
refute :: Bool -> Result -> IO Int;
refute genuine_only r = ref genuine_only r (args r);
sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int;
sumMapM f n [] = return n;
sumMapM f n (a:as) = seq n (do m <- f a ; sumMapM f (n+m) as);
-- Testable
instance Show Typerep.Typerep where {
show (Typerep.Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
};
instance Show Generated_Code.Term where {
show (Generated_Code.Const c t) = "Const (\"" ++ c ++ "\", " ++ show t ++ ")";
show (Generated_Code.App s t) = "(" ++ show s ++ ") $ (" ++ show t ++ ")";
show (Generated_Code.Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")";
show (Generated_Code.Free s ty) = "Free (\"" ++ s ++ "\", " ++ show ty ++ ")";
};
data Result =
Result { args :: [Generated_Code.Narrowing_term]
, showArgs :: [Generated_Code.Narrowing_term -> String]
, apply_fun :: [Generated_Code.Narrowing_term] -> Bool
};
data P = P (Int -> Int -> Result);
run :: Testable a => ([Generated_Code.Narrowing_term] -> a) -> Int -> Int -> Result;
run a = let P f = property a in f;
class Testable a where {
property :: ([Generated_Code.Narrowing_term] -> a) -> P;
};
instance Testable Bool where {
property app = P $ \n d -> Result [] [] (app . reverse);
};
instance (Generated_Code.Partial_term_of a, Generated_Code.Narrowing a, Testable b) => Testable (a -> b) where {
property f = P $ \n d ->
let Generated_Code.Narrowing_cons t c = Generated_Code.narrowing d
c' = Generated_Code.conv c
r = run (\(x:xs) -> f xs (c' x)) (n+1) d
in r { args = Generated_Code.Narrowing_variable [n] t : args r,
showArgs = (show . Generated_Code.partial_term_of (Generated_Code.Type :: Generated_Code.Itself a)) : showArgs r };
};
-- Top-level interface
depthCheck :: Testable a => Bool -> Int -> a -> IO ();
depthCheck genuine_only d p =
(refute genuine_only $ run (const p) 0 d) >> putStrLn ("NONE") >> hFlush stdout;
smallCheck :: Testable a => Bool -> Int -> a -> IO ();
smallCheck genuine_only d p = mapM_ (\d -> depthCheck genuine_only d p) [0..d] >> putStrLn ("NONE") >> hFlush stdout;
}
module Typerep where {
data Typerep = Typerep String [Typerep]
}
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
