Hets - the Heterogeneous Tool Set

Copyright(c) C. Maeder DFKI 2008
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellNone

Comorphisms.PPolyTyConsHOL2IsaUtils

Description

utility function for translation from HasCASL to Isabelle leaving open how partial values are interpreted

Documentation

mapTheory :: SimpKind -> Simplifier -> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #

simpForPairs :: Simplifier Source #

simpForOption :: Simplifier Source #

typeToks :: Env -> Set String Source #

transSentence :: Env -> Set String -> SimpKind -> Simplifier -> Sentence -> Result Sentence Source #

data SimpKind Source #

Constructors

New 
Old OldSimpKind 

Instances

Eq SimpKind Source # 

Methods

(==) :: SimpKind -> SimpKind -> Bool

(/=) :: SimpKind -> SimpKind -> Bool

data OldSimpKind Source #

Instances

Eq OldSimpKind Source # 

Methods

(==) :: OldSimpKind -> OldSimpKind -> Bool

(/=) :: OldSimpKind -> OldSimpKind -> Bool