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

Instances details
Eq SimpKind Source # 
Instance details

Defined in Comorphisms.PPolyTyConsHOL2IsaUtils

Methods

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

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

data OldSimpKind Source #

Constructors

NoSimpLift 
Lift2Restrict 
Lift2Case 

Instances

Instances details
Eq OldSimpKind Source # 
Instance details

Defined in Comorphisms.PPolyTyConsHOL2IsaUtils

Methods

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

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