Hets - the Heterogeneous Tool Set

Copyright	(c) Dominik Dietrich DFKI Bremen 2010
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Dominik.Dietrich@dfki.de
Stability	provisional
Portability	portable
Safe Haskell	Safe

CSL.Lemma_Export

Description

Interface for Reduce CAS system.

Synopsis

ganame :: Named CMD -> String
genLemmaFactor :: Named CMD -> EXPRESSION -> Named CMD
genLemmaSolve :: Named CMD -> EXPRESSION -> Named CMD
genLemmaSimplify :: Named CMD -> EXPRESSION -> Named CMD
genLemmaAsk :: Named CMD -> EXPRESSION -> Named CMD
genLemmaRemainder :: Named CMD -> EXPRESSION -> Named CMD
genLemmaInt :: Named CMD -> EXPRESSION -> Named CMD

Documentation

ganame :: Named CMD -> String Source #

generate name for generated lemma out of name of theorem

genLemmaFactor :: Named CMD -> EXPRESSION -> Named CMD Source #

generates lemma in form of a named CMD for namedcmd that resulted in CAS answer casresult

genLemmaSolve :: Named CMD -> EXPRESSION -> Named CMD Source #

generates lemma in form of a named CMD for namedcmd that resulted in CAS answer casresult

genLemmaSimplify :: Named CMD -> EXPRESSION -> Named CMD Source #

generates lemma in form of a named CMD for namedcmd that resulted in CAS answer casresult

genLemmaAsk :: Named CMD -> EXPRESSION -> Named CMD Source #

generates lemma in form of a named CMD for namedcmd that resulted in CAS answer casresult

genLemmaRemainder :: Named CMD -> EXPRESSION -> Named CMD Source #

generates lemma in form of a named CMD for namedcmd that resulted in CAS answer casresult

genLemmaInt :: Named CMD -> EXPRESSION -> Named CMD Source #

generates lemma in form of a named CMD for namedcmd that resulted in CAS answer casresult