Documentation

primCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2, MonadFail m) => lid1 -> lid2 -> String -> a -> m b Source #

unsafeCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2) => lid1 -> lid2 -> a -> b Source #

coerceToResult :: (Typeable a, Typeable b, Language lid1, Language lid2) => lid1 -> lid2 -> Range -> a -> Result b Source #

coerceSublogic :: (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, MonadFail m) => lid1 -> lid2 -> String -> sublogics1 -> m sublogics2 Source #

forceCoerceSublogic :: (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2) => lid1 -> lid2 -> sublogics1 -> sublogics2 Source #

coercePlainSign :: (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, MonadFail m) => lid1 -> lid2 -> String -> sign1 -> m sign2 Source #

coerceSign :: (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, MonadFail m) => lid1 -> lid2 -> String -> ExtSign sign1 symbol1 -> m (ExtSign sign2 symbol2) Source #

coerceBasicTheory :: (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, MonadFail m) => lid1 -> lid2 -> String -> (sign1, [Named sentence1]) -> m (sign2, [Named sentence2]) Source #

coerceTheoryMorphism :: (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, MonadFail m) => lid1 -> lid2 -> String -> TheoryMorphism sign1 sentence1 morphism1 proof_tree1 -> m (TheoryMorphism sign2 sentence2 morphism2 proof_tree2) Source #

coerceSens :: (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, MonadFail m) => lid1 -> lid2 -> String -> [Named sentence1] -> m [Named sentence2] Source #

coerceMorphism :: (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, MonadFail m) => lid1 -> lid2 -> String -> morphism1 -> m morphism2 Source #

coerceSymbol :: (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2) => lid1 -> lid2 -> symbol1 -> symbol2 Source #

coerceSymbolmap :: (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, Typeable a) => lid1 -> lid2 -> Map symbol1 a -> Map symbol2 a Source #

coerceMapofsymbol :: (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, Typeable a) => lid1 -> lid2 -> Map a symbol1 -> Map a symbol2 Source #

coerceSymbItemsList :: (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, MonadFail m) => lid1 -> lid2 -> String -> [symb_items1] -> m [symb_items2] Source #

coerceSymbMapItemsList :: (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, MonadFail m) => lid1 -> lid2 -> String -> [symb_map_items1] -> m [symb_map_items2] Source #

coerceProofStatus :: (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, MonadFail m) => lid1 -> lid2 -> String -> ProofStatus proof_tree1 -> m (ProofStatus proof_tree2) Source #

coerceSymbolSet :: (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, MonadFail m) => lid1 -> lid2 -> String -> Set symbol1 -> m (Set symbol2) Source #

coerceRawSymbolMap :: (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, MonadFail m) => lid1 -> lid2 -> String -> EndoMap raw_symbol1 -> m (EndoMap raw_symbol2) Source #

coerceFreeDefMorphism :: (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, MonadFail m) => lid1 -> lid2 -> String -> FreeDefMorphism sentence1 morphism1 -> m (FreeDefMorphism sentence2 morphism2) Source #