Documentation

migrateLogicGraphKey :: String Source #

exportLogicGraph :: HetcatsOpts -> IO () Source #

findOrCreateLogic :: (MonadIO m, Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree) => HetcatsOpts -> LanguageId -> lid -> sublogics -> DBMonad m LogicId Source #

findOrCreateLanguageMappingAndLogicMapping :: (MonadIO m, MonadFail m) => HetcatsOpts -> AnyComorphism -> DBMonad m (LanguageMappingId, LogicMappingId) Source #

findReasoner :: MonadIO m => String -> ReasonerKindType -> DBMonad m (Maybe (Entity Reasoner)) Source #

findOrCreateProver :: MonadIO m => G_prover -> DBMonad m ReasonerId Source #

findOrCreateConsistencyChecker :: MonadIO m => G_cons_checker -> DBMonad m ReasonerId Source #

findLogicMappingByComorphism :: (MonadIO m, MonadFail m) => AnyComorphism -> DBMonad m (Maybe (Entity LogicMapping)) Source #

findOrCreateLogicTranslation :: (MonadIO m, MonadFail m) => HetcatsOpts -> AnyComorphism -> DBMonad m (Maybe (Entity LogicTranslation)) Source #

findReasonerByProverOrConsChecker :: (MonadIO m, MonadFail m) => ProverOrConsChecker -> DBMonad m (Entity Reasoner) Source #

findReasonerByGConsChecker :: (MonadIO m, MonadFail m) => G_cons_checker -> DBMonad m (Entity Reasoner) Source #

findReasonerByGProver :: (MonadIO m, MonadFail m) => G_prover -> DBMonad m (Entity Reasoner) Source #