Re: [isabelle] Dependencies on constants



Am 23.06.2010 um 18:44 schrieb Rafal Kolanski:

> I've investigated Spec_Rules. It works as advertised for "definition" and "constdefs", however the primrec/recdef/function/fun sadly do not register their constants in this manner.

What??

    $ grep -l Spec_Rules ~/isabelle/src/HOL/Tools/*{,/*}
    /Users/blanchet/isabelle/src/HOL/Tools/inductive.ML
    /Users/blanchet/isabelle/src/HOL/Tools/old_primrec.ML
    /Users/blanchet/isabelle/src/HOL/Tools/primrec.ML
    /Users/blanchet/isabelle/src/HOL/Tools/recdef.ML
    /Users/blanchet/isabelle/src/HOL/Tools/Function/function.ML
    /Users/blanchet/isabelle/src/HOL/Tools/Function/size.ML
    /Users/blanchet/isabelle/src/HOL/Tools/Nitpick/nitpick_hol.ML
    /Users/blanchet/isabelle/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML

I see primrec, recdef, and function/fun in there. Lukas's predicate compiler uses "Spec_Rules" to find equational specifications, so it must be working. Nitpick uses it already for the "(co)inductive" package and it's definitely working.

Cheers,

Jasmin






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.