44c016134fdac329e51c993f040a40cd9eb3ee6bTinderbox User{- |

44c016134fdac329e51c993f040a40cd9eb3ee6bTinderbox UserModule : $EmptyHeader$

44c016134fdac329e51c993f040a40cd9eb3ee6bTinderbox UserDescription : <optional short description entry>

44c016134fdac329e51c993f040a40cd9eb3ee6bTinderbox UserCopyright : (c) <Authors or Affiliations>

44c016134fdac329e51c993f040a40cd9eb3ee6bTinderbox UserLicense : GPLv2 or higher, see LICENSE.txt

44c016134fdac329e51c993f040a40cd9eb3ee6bTinderbox User

44c016134fdac329e51c993f040a40cd9eb3ee6bTinderbox UserMaintainer : <email>

44c016134fdac329e51c993f040a40cd9eb3ee6bTinderbox UserStability : unstable | experimental | provisional | stable | frozen

44c016134fdac329e51c993f040a40cd9eb3ee6bTinderbox UserPortability : portable | non-portable (<reason>)

44c016134fdac329e51c993f040a40cd9eb3ee6bTinderbox User

44c016134fdac329e51c993f040a40cd9eb3ee6bTinderbox User<optional description>

44c016134fdac329e51c993f040a40cd9eb3ee6bTinderbox User-}

44c016134fdac329e51c993f040a40cd9eb3ee6bTinderbox Usermodule Structured (module Structured, module Grothendieck) where

0b4ed61d201b32a4abc773707238bcbfc157835aEvan Hunt

0b4ed61d201b32a4abc773707238bcbfc157835aEvan Huntimport Grothendieck

0b4ed61d201b32a4abc773707238bcbfc157835aEvan Hunt

data SPEC = Basic_spec G_basic_spec -- unstructured specifications

| Intra_Translation SPEC G_symbol_mapping_list -- renaming within a logic

| Inter_Translation SPEC AnyTranslation -- translation between logics

| Extension SPEC SPEC -- hierarchical extension or union

deriving Show

data Env = Basic_env G_theory

| Intra_Translation_env G_theory Env G_morphism

| Inter_Translation_env G_theory Env AnyTranslation

| Extension_env G_theory Env Env