Index
| $-$ | Tip.Pretty.Isabelle |
| $\ | Tip.Pretty |
| // | Tip.Core |
| /\ | Tip.Core |
| :+: | Tip.Core |
| ::: | Tip.Haskell.Repr |
| :=>: | Tip.Types, Tip.Core |
| :@: | Tip.Types, Tip.Core |
| =/= | Tip.Core |
| === | Tip.Core |
| ===> | Tip.Core |
| ==> | Tip.Core |
| absurd | Tip.Utils.Specialiser |
| addHeader | Tip.Haskell.Translate |
| addImports | Tip.Haskell.Translate |
| AddMatch | Tip.Passes |
| addMatch | Tip.Passes |
| aggressively | Tip.Simplify, Tip.Passes |
| And | Tip.Types, Tip.Core |
| ands | Tip.Core |
| Apply | Tip.Haskell.Repr |
| apply | |
| 1 (Function) | Tip.Core |
| 2 (Function) | Tip.Pretty.SMT |
| 3 (Function) | Tip.Pretty.TFF |
| applyFunction | Tip.Core |
| applyPolyType | Tip.Core |
| applySignature | Tip.Core |
| applyType | Tip.Core |
| applyTypeIn | Tip.Core |
| applyTypeInDecl | Tip.Core |
| applyTypeInExpr | Tip.Core |
| arbitrary | Tip.Haskell.Translate |
| Assert | Tip.Types, Tip.Core |
| AssertDecl | Tip.Types, Tip.Core |
| At | Tip.Types, Tip.Core |
| atomic | Tip.Core |
| AxiomatizeDatadecls | Tip.Passes |
| axiomatizeDatadecls | Tip.Passes |
| AxiomatizeDatadeclsUEQ | Tip.Passes |
| AxiomatizeFuncdefs | Tip.Passes |
| axiomatizeFuncdefs | Tip.Passes |
| AxiomatizeFuncdefs2 | Tip.Passes |
| axiomatizeFuncdefs2 | Tip.Passes |
| AxiomatizeLambdas | Tip.Passes |
| axiomatizeLambdas | Tip.Passes |
| Bind | Tip.Haskell.Repr |
| BindTyped | Tip.Haskell.Repr |
| Block | |
| 1 (Type/Class) | Tip.CallGraph |
| 2 (Data Constructor) | Tip.CallGraph |
| block | |
| 1 (Function) | Tip.Pretty.Why3 |
| 2 (Function) | Tip.Pretty.Isabelle |
| Bool | Tip.Types, Tip.Core |
| bool | Tip.Core |
| Boolean | Tip.Types, Tip.Core |
| boolExpr | Tip.Pass.Booleans |
| boolGbl | Tip.Pass.Booleans |
| boolName | Tip.Pass.Booleans |
| BoolNames | |
| 1 (Type/Class) | Tip.Pass.Booleans |
| 2 (Data Constructor) | Tip.Pass.Booleans |
| BoolOpLift | Tip.Passes |
| boolOpLift | Tip.Passes |
| BoolOpToIf | Tip.Passes |
| boolOpToIf | Tip.Pass.Booleans, Tip.Passes |
| boolType | Tip.Core |
| boolView | Tip.Core |
| bound | Tip.Core |
| Builtin | |
| 1 (Type/Class) | Tip.Types, Tip.Core |
| 2 (Data Constructor) | Tip.Types, Tip.Core |
| BuiltinType | |
| 1 (Type/Class) | Tip.Types, Tip.Core |
| 2 (Data Constructor) | Tip.Types, Tip.Core |
| builtinType | Tip.Core |
| callees | Tip.CallGraph |
| callers | Tip.CallGraph |
| callGraph | Tip.CallGraph |
| CallGraphOpts | |
| 1 (Type/Class) | Tip.CallGraph |
| 2 (Data Constructor) | Tip.CallGraph |
| Case | |
| 1 (Data Constructor) | Tip.Haskell.Repr |
| 2 (Type/Class) | Tip.Types, Tip.Core |
| 3 (Data Constructor) | Tip.Types, Tip.Core |
| case_pat | Tip.Types, Tip.Core |
| case_rhs | Tip.Types, Tip.Core |
| censor | Tip.Writer |
| checkScope | Tip.Scope |
| checkScopeT | Tip.Scope |
| Choice | Tip.Passes |
| choice | Tip.Passes |
| ClassDecl | Tip.Haskell.Repr |
| clause | Tip.Pretty.TFF |
| Closed | Tip.Utils.Specialiser |
| CollapseEqual | Tip.Passes |
| collapseEqual | Tip.Passes |
| collectLets | Tip.Core |
| CommuteMatch | Tip.Passes |
| commuteMatch | Tip.Passes |
| Component | Tip.Utils |
| components | Tip.Utils |
| Con | Tip.Utils.Specialiser |
| ConPat | |
| 1 (Data Constructor) | Tip.Haskell.Repr |
| 2 (Data Constructor) | Tip.Types, Tip.Core |
| Constructor | |
| 1 (Type/Class) | Tip.Types, Tip.Core |
| 2 (Data Constructor) | Tip.Types, Tip.Core |
| constructor | Tip.Core |
| ConstructorInfo | Tip.Scope |
| constructorType | Tip.Core |
| continuePasses | Tip.Passes |
| con_args | Tip.Types, Tip.Core |
| con_discrim | Tip.Types, Tip.Core |
| con_name | Tip.Types, Tip.Core |
| CSEMatch | Tip.Passes |
| cseMatch | Tip.Passes |
| cseMatchNormal | Tip.Passes |
| CSEMatchWhy3 | Tip.Passes |
| cseMatchWhy3 | Tip.Passes |
| csv | |
| 1 (Function) | Tip.Pretty.Why3 |
| 2 (Function) | Tip.Pretty.Isabelle |
| 3 (Function) | Tip.Pretty.Haskell |
| csv1 | |
| 1 (Function) | Tip.Pretty.Why3 |
| 2 (Function) | Tip.Pretty.Isabelle |
| cursor | Tip.Utils |
| DataDecl | |
| 1 (Data Constructor) | Tip.Haskell.Repr |
| 2 (Data Constructor) | Tip.Types, Tip.Core |
| DataDistinct | Tip.Types, Tip.Core |
| DataDomain | Tip.Types, Tip.Core |
| DataProjection | Tip.Types, Tip.Core |
| Datatype | |
| 1 (Type/Class) | Tip.Types, Tip.Core |
| 2 (Data Constructor) | Tip.Types, Tip.Core |
| DatatypeInfo | Tip.Scope |
| data_cons | Tip.Types, Tip.Core |
| data_name | Tip.Types, Tip.Core |
| data_tvs | Tip.Types, Tip.Core |
| Decl | |
| 1 (Type/Class) | Tip.Haskell.Repr |
| 2 (Type/Class) | Tip.Types, Tip.Core |
| Decls | |
| 1 (Type/Class) | Tip.Haskell.Repr |
| 2 (Data Constructor) | Tip.Haskell.Repr |
| declsPass | Tip.Types, Tip.Core |
| declsToTheory | Tip.Types, Tip.Core |
| DeepConPat | Tip.Core |
| DeepLitPat | Tip.Core |
| DeepPattern | Tip.Core |
| DeepVarPat | Tip.Core |
| Default | Tip.Types, Tip.Core |
| defines | Tip.Core |
| Definition | |
| 1 (Data Constructor) | Tip.Types, Tip.Core |
| 2 (Type/Class) | Tip.Core |
| Defunction | Tip.Types, Tip.Core |
| DeleteConjecture | Tip.Passes |
| deleteConjecture | Tip.Passes |
| Derived | Tip.Haskell.Translate |
| destructorType | Tip.Core |
| disambig | Tip.Utils.Rename |
| disambig2 | Tip.Utils.Rename |
| discriminator | Tip.Core |
| DiscriminatorInfo | Tip.Scope |
| Distinct | Tip.Types, Tip.Core |
| Do | Tip.Haskell.Repr |
| DropSuffix | Tip.Passes |
| dropSuffix | Tip.Passes |
| duplicates | Tip.Utils |
| EliminateDeadCode | Tip.Passes |
| emptyScope | Tip.Scope |
| emptyTheory | Tip.Types, Tip.Core |
| eqRelatedBuiltin | Tip.Types, Tip.Core |
| Equal | Tip.Types, Tip.Core |
| escape | |
| 1 (Function) | Tip.Pretty.Why3 |
| 2 (Function) | Tip.Pretty.Isabelle |
| evalRenameM | Tip.Utils.Rename |
| Exact | Tip.Haskell.Translate |
| Exists | Tip.Types, Tip.Core |
| exploreCalleesFirst | Tip.CallGraph |
| exploreSingleFunctions | Tip.CallGraph |
| Expr | |
| 1 (Type/Class) | Tip.Haskell.Repr |
| 2 (Type/Class) | Tip.Types, Tip.Core |
| 3 (Type/Class) | Tip.Utils.Specialiser |
| 4 (Data Constructor) | Tip.Haskell.Translate |
| expr | Tip.Pretty.SMT |
| exprSep | Tip.Pretty.SMT |
| exprType | Tip.Core |
| falseExpr | Tip.Core |
| falseName | Tip.Pass.Booleans |
| Feat | Tip.Haskell.Translate, Tip.Pretty.Haskell |
| feat | Tip.Haskell.Translate |
| fillInCases | Tip.Passes |
| First | Tip.Passes |
| flagify | Tip.Utils |
| flagifyShow | Tip.Utils |
| flatCallGraph | Tip.CallGraph |
| flattenBlock | Tip.CallGraph |
| flattenComponent | Tip.Utils |
| fm_body | Tip.Types, Tip.Core |
| fm_info | Tip.Types, Tip.Core |
| fm_role | Tip.Types, Tip.Core |
| fm_tvs | Tip.Types, Tip.Core |
| Forall | Tip.Types, Tip.Core |
| forallView | Tip.Core |
| Formula | |
| 1 (Type/Class) | Tip.Types, Tip.Core |
| 2 (Data Constructor) | Tip.Types, Tip.Core |
| 3 (Data Constructor) | Tip.Haskell.Translate |
| formulaBoolOpToIf | Tip.Pass.Booleans |
| free | Tip.Core |
| freeTyVars | Tip.Core |
| Fresh | |
| 1 (Type/Class) | Tip.Fresh |
| 2 (Data Constructor) | Tip.Fresh |
| fresh | Tip.Fresh |
| freshArgs | Tip.Core |
| freshBoolNames | Tip.Pass.Booleans |
| freshen | Tip.Core |
| freshenNames | Tip.Core |
| freshFrom | Tip.Fresh |
| freshLocal | Tip.Core |
| freshNamed | Tip.Fresh |
| freshPass | Tip.Fresh, Tip.Passes |
| FS | Tip.CallGraph |
| FuncDecl | Tip.Types, Tip.Core |
| Function | |
| 1 (Type/Class) | Tip.Types, Tip.Core |
| 2 (Data Constructor) | Tip.Types, Tip.Core |
| FunctionInfo | Tip.Scope |
| funcType | Tip.Core |
| func_args | Tip.Types, Tip.Core |
| func_body | Tip.Types, Tip.Core |
| func_name | Tip.Types, Tip.Core |
| func_res | Tip.Types, Tip.Core |
| func_tvs | Tip.Types, Tip.Core |
| FunDecl | Tip.Haskell.Repr |
| funDecl | Tip.Haskell.Repr |
| Gbl | Tip.Types, Tip.Core |
| gblType | Tip.Core |
| gbl_args | Tip.Types, Tip.Core |
| gbl_name | Tip.Types, Tip.Core |
| gbl_type | Tip.Types, Tip.Core |
| gentleNeg | Tip.Core |
| gently | Tip.Simplify, Tip.Passes |
| gentlyNoInline | Tip.Simplify |
| getUnique | Tip.Fresh |
| Global | |
| 1 (Type/Class) | Tip.Types, Tip.Core |
| 2 (Data Constructor) | Tip.Types, Tip.Core |
| GlobalInfo | Tip.Scope |
| globals | |
| 1 (Function) | Tip.Core |
| 2 (Function) | Tip.Scope |
| globalType | Tip.Scope |
| hasBoolType | Tip.Pass.Booleans |
| Head | Tip.Types, Tip.Core |
| hsBuiltins | Tip.Haskell.Translate |
| hsBuiltinTys | Tip.Haskell.Translate |
| HsId | Tip.Haskell.Translate |
| Id | Tip.Parser |
| idPos | Tip.Parser |
| IfToBoolOp | Tip.Passes |
| ifToBoolOp | Tip.Pass.Booleans, Tip.Passes |
| ifView | Tip.Core |
| IH | Tip.Types, Tip.Core |
| ImpLet | Tip.Haskell.Repr |
| Implies | Tip.Types, Tip.Core |
| ImpVar | Tip.Haskell.Repr |
| inContext | Tip.Scope |
| Induction | Tip.Passes |
| induction | Tip.Passes |
| Info | Tip.Types, Tip.Core |
| InL | Tip.Core |
| inline_match | Tip.Simplify, Tip.Passes |
| inner | Tip.Scope |
| InR | Tip.Core |
| insert | Tip.Utils.Rename |
| insertMany | Tip.Utils.Rename |
| Inst | Tip.Utils.Specialiser |
| InstDecl | Tip.Haskell.Repr |
| Int | |
| 1 (Data Constructor) | Tip.Haskell.Repr |
| 2 (Data Constructor) | Tip.Types, Tip.Core |
| IntAdd | Tip.Types, Tip.Core |
| intBuiltin | Tip.Types, Tip.Core |
| IntDiv | Tip.Types, Tip.Core |
| Integer | Tip.Types, Tip.Core |
| intersperseWithPre | Tip.Pretty.Isabelle |
| IntGe | Tip.Types, Tip.Core |
| IntGt | Tip.Types, Tip.Core |
| IntLe | Tip.Types, Tip.Core |
| intLit | Tip.Core |
| IntLt | Tip.Types, Tip.Core |
| IntMod | Tip.Types, Tip.Core |
| IntMul | Tip.Types, Tip.Core |
| IntPat | Tip.Haskell.Repr |
| IntSub | Tip.Types, Tip.Core |
| IntToNat | Tip.Passes |
| intToNat | Tip.Passes |
| intType | Tip.Core |
| isabelleKeywords | Tip.Pretty.Isabelle |
| isConstructor | Tip.Simplify |
| isFalseName | Tip.Pass.Booleans |
| isGlobal | Tip.Scope |
| isLazySmallCheck | Tip.Haskell.Translate |
| isLocal | Tip.Scope |
| isOp | Tip.Pretty.Haskell |
| isOperator | Tip.Haskell.Rename |
| isSmten | Tip.Haskell.Translate |
| isSort | Tip.Scope |
| isTrueName | Tip.Pass.Booleans |
| isType | Tip.Scope |
| isTyVar | Tip.Scope |
| joinTheories | Tip.Types, Tip.Core |
| keywords | Tip.Pretty.Waldmeister |
| Kind | Tip.Haskell.Translate |
| Lam | |
| 1 (Data Constructor) | Tip.Haskell.Repr |
| 2 (Data Constructor) | Tip.Types, Tip.Core |
| LambdaLift | Tip.Passes |
| lambdaLift | Tip.Passes |
| LANGUAGE | Tip.Haskell.Repr |
| LazySmallCheck | Tip.Haskell.Translate, Tip.Pretty.Haskell |
| Lcl | Tip.Types, Tip.Core |
| lcl_name | Tip.Types, Tip.Core |
| lcl_type | Tip.Types, Tip.Core |
| Lemma | Tip.Types, Tip.Core |
| Let | |
| 1 (Data Constructor) | Tip.Haskell.Repr |
| 2 (Data Constructor) | Tip.Types, Tip.Core |
| letExpr | Tip.Core |
| LetLift | Tip.Passes |
| letLift | Tip.Passes |
| lift | Tip.Writer |
| lint | Tip.Lint |
| lintEither | Tip.Lint |
| lintM | Tip.Lint |
| lintMany | Tip.Passes |
| lintTheory | Tip.Lint |
| List | Tip.Haskell.Repr |
| Lit | |
| 1 (Type/Class) | Tip.Types, Tip.Core |
| 2 (Data Constructor) | Tip.Types, Tip.Core |
| litBuiltin | Tip.Types, Tip.Core |
| literal | Tip.Core |
| LitPat | Tip.Types, Tip.Core |
| litView | Tip.Core |
| lkup | Tip.Utils.Rename |
| Local | |
| 1 (Type/Class) | Tip.Types, Tip.Core |
| 2 (Data Constructor) | Tip.Types, Tip.Core |
| local | Tip.Scope |
| locals | |
| 1 (Function) | Tip.Core |
| 2 (Function) | Tip.Scope |
| logicalBuiltin | Tip.Types, Tip.Core |
| lookupComponent | Tip.Utils |
| lookupConstructor | Tip.Scope |
| lookupDatatype | Tip.Scope |
| lookupDiscriminator | Tip.Scope |
| lookupFunction | Tip.Scope |
| lookupGlobal | Tip.Scope |
| lookupLocal | Tip.Scope |
| lookupProjector | Tip.Scope |
| lookupType | Tip.Scope |
| lsc | Tip.Haskell.Translate |
| MakeConjecture | Tip.Passes |
| makeConjecture | Tip.Passes |
| makeGlobal | Tip.Core |
| makeIf | Tip.Core |
| makeLets | Tip.Core |
| makeSig | Tip.Haskell.Translate |
| mapDecls | Tip.Core |
| Match | Tip.Types, Tip.Core |
| matchTypes | Tip.Core |
| matchTypesIn | Tip.Core |
| maximumOn | Tip.Utils |
| missingCase | Tip.Simplify |
| mkDo | Tip.Haskell.Repr |
| mkQuant | Tip.Core |
| Mode | Tip.Haskell.Translate, Tip.Pretty.Haskell |
| modTyCon | Tip.Haskell.Repr |
| Module | Tip.Haskell.Repr |
| Monomorphise | Tip.Passes |
| monomorphise | Tip.Passes |
| Name | Tip.Fresh |
| neg | Tip.Core |
| NegateConjecture | Tip.Passes |
| negateConjecture | Tip.Passes |
| nestedTup | Tip.Haskell.Repr |
| nestedTupPat | Tip.Haskell.Repr |
| nestedTyTup | Tip.Haskell.Repr |
| newConstructor | Tip.Scope |
| newDatatype | Tip.Scope |
| newFunction | Tip.Scope |
| newLocal | Tip.Scope |
| newName | Tip.Scope |
| newScope | Tip.Scope |
| newSort | Tip.Scope |
| newTyVar | Tip.Scope |
| NoInfo | Tip.Types, Tip.Core |
| NonRec | Tip.Utils |
| Noop | Tip.Haskell.Repr |
| Not | Tip.Types, Tip.Core |
| Occurrences | |
| 1 (Type/Class) | Tip.Simplify |
| 2 (Data Constructor) | Tip.Simplify |
| occurrences | Tip.Core |
| oppositeQuant | Tip.Core |
| Or | Tip.Types, Tip.Core |
| ors | Tip.Core |
| Other | Tip.Haskell.Translate |
| par | Tip.Pretty.SMT |
| par' | Tip.Pretty.SMT |
| par'' | Tip.Pretty.SMT |
| parExpr | Tip.Pretty.SMT |
| parExprSep | Tip.Pretty.SMT |
| parIf | Tip.Pretty |
| parse | Tip.Parser |
| parseFile | Tip.Parser |
| parsePass | Tip.Passes |
| parsePasses | Tip.Passes |
| partitionGoals | Tip.Core |
| Pass | Tip.Passes |
| passName | Tip.Passes |
| Pat | Tip.Haskell.Repr |
| Pattern | Tip.Types, Tip.Core |
| patternMatchingView | Tip.Core |
| pat_args | Tip.Types, Tip.Core |
| pat_con | Tip.Types, Tip.Core |
| pcsv | |
| 1 (Function) | Tip.Pretty.Why3 |
| 2 (Function) | Tip.Pretty.Isabelle |
| Plain | Tip.Haskell.Translate, Tip.Pretty.Haskell |
| PolyType | |
| 1 (Type/Class) | Tip.Types, Tip.Core |
| 2 (Data Constructor) | Tip.Types, Tip.Core |
| polytype_args | Tip.Types, Tip.Core |
| polytype_res | Tip.Types, Tip.Core |
| polytype_tvs | Tip.Types, Tip.Core |
| pp | Tip.Pretty |
| ppAsTuple | Tip.Pretty.Isabelle |
| ppBinder | |
| 1 (Function) | Tip.Pretty.Why3 |
| 2 (Function) | Tip.Pretty.Isabelle |
| ppBinOp | |
| 1 (Function) | Tip.Pretty.Why3 |
| 2 (Function) | Tip.Pretty.Isabelle |
| ppBuiltin | |
| 1 (Function) | Tip.Pretty.SMT |
| 2 (Function) | Tip.Pretty.Why3 |
| 3 (Function) | Tip.Pretty.Isabelle |
| 4 (Function) | Tip.Pretty.TFF |
| ppBuiltinType | |
| 1 (Function) | Tip.Pretty.SMT |
| 2 (Function) | Tip.Pretty.TFF |
| ppCase | |
| 1 (Function) | Tip.Pretty.SMT |
| 2 (Function) | Tip.Pretty.Why3 |
| 3 (Function) | Tip.Pretty.Isabelle |
| ppCon | |
| 1 (Function) | Tip.Pretty.SMT |
| 2 (Function) | Tip.Pretty.Why3 |
| 3 (Function) | Tip.Pretty.Isabelle |
| ppData | |
| 1 (Function) | Tip.Pretty.SMT |
| 2 (Function) | Tip.Pretty.Why3 |
| 3 (Function) | Tip.Pretty.Isabelle |
| ppDatas | |
| 1 (Function) | Tip.Pretty.SMT |
| 2 (Function) | Tip.Pretty.Why3 |
| 3 (Function) | Tip.Pretty.Isabelle |
| ppDeepPattern | |
| 1 (Function) | Tip.Pretty.Why3 |
| 2 (Function) | Tip.Pretty.Isabelle |
| ppExpr | |
| 1 (Function) | Tip.Pretty.SMT |
| 2 (Function) | Tip.Pretty.Why3 |
| 3 (Function) | Tip.Pretty.Isabelle |
| 4 (Function) | Tip.Pretty.TFF |
| 5 (Function) | Tip.Pretty.Waldmeister |
| ppFormula | |
| 1 (Function) | Tip.Pretty.SMT |
| 2 (Function) | Tip.Pretty.Why3 |
| 3 (Function) | Tip.Pretty.Isabelle |
| 4 (Function) | Tip.Pretty.TFF |
| 5 (Function) | Tip.Pretty.Waldmeister |
| ppFunc | |
| 1 (Function) | Tip.Pretty.Why3 |
| 2 (Function) | Tip.Pretty.Isabelle |
| ppFuncs | |
| 1 (Function) | Tip.Pretty.SMT |
| 2 (Function) | Tip.Pretty.Why3 |
| 3 (Function) | Tip.Pretty.Isabelle |
| ppFuncSig | Tip.Pretty.SMT |
| ppHead | |
| 1 (Function) | Tip.Pretty.SMT |
| 2 (Function) | Tip.Pretty.Why3 |
| 3 (Function) | Tip.Pretty.Isabelle |
| 4 (Function) | Tip.Pretty.TFF |
| 5 (Function) | Tip.Pretty.Waldmeister |
| ppHsVar | Tip.Pretty.Haskell |
| ppLit | |
| 1 (Function) | Tip.Pretty.SMT |
| 2 (Function) | Tip.Pretty.Why3 |
| 3 (Function) | Tip.Pretty.Isabelle |
| 4 (Function) | Tip.Pretty.TFF |
| ppLocal | |
| 1 (Function) | Tip.Pretty.SMT |
| 2 (Function) | Tip.Pretty.TFF |
| ppLocalBinder | |
| 1 (Function) | Tip.Pretty.Why3 |
| 2 (Function) | Tip.Pretty.Isabelle |
| ppLocals | Tip.Pretty.SMT |
| ppOper | Tip.Pretty.Haskell |
| ppOperQ | Tip.Pretty.Haskell |
| ppPat | |
| 1 (Function) | Tip.Pretty.SMT |
| 2 (Function) | Tip.Pretty.Why3 |
| 3 (Function) | Tip.Pretty.Isabelle |
| 4 (Function) | Tip.Pretty.Haskell |
| ppPolyType | Tip.Pretty.SMT |
| ppQuant | |
| 1 (Function) | Tip.Pretty.SMT |
| 2 (Function) | Tip.Pretty.Why3 |
| 3 (Function) | Tip.Pretty.Isabelle |
| 4 (Function) | Tip.Pretty.TFF |
| ppQuantName | |
| 1 (Function) | Tip.Pretty.Why3 |
| 2 (Function) | Tip.Pretty.Isabelle |
| ppRender | Tip.Pretty |
| pprint | Tip.Pretty |
| ppRole | |
| 1 (Function) | Tip.Pretty.Why3 |
| 2 (Function) | Tip.Pretty.Isabelle |
| ppSig | Tip.Pretty.Waldmeister |
| ppSort | |
| 1 (Function) | Tip.Pretty.SMT |
| 2 (Function) | Tip.Pretty.Why3 |
| 3 (Function) | Tip.Pretty.Isabelle |
| 4 (Function) | Tip.Pretty.TFF |
| ppTheory | |
| 1 (Function) | Tip.Pretty.SMT |
| 2 (Function) | Tip.Pretty.Why3 |
| 3 (Function) | Tip.Pretty.Isabelle |
| 4 (Function) | Tip.Pretty.TFF |
| 5 (Function) | Tip.Pretty.Waldmeister |
| 6 (Function) | Tip.Pretty.Haskell |
| ppTheoryWithRenamings | Tip.Pretty.Haskell |
| ppType | |
| 1 (Function) | Tip.Pretty.SMT |
| 2 (Function) | Tip.Pretty.Why3 |
| 3 (Function) | Tip.Pretty.Isabelle |
| 4 (Function) | Tip.Pretty.TFF |
| 5 (Function) | Tip.Pretty.Waldmeister |
| 6 (Function) | Tip.Pretty.Haskell |
| ppTyVar | |
| 1 (Function) | Tip.Pretty.Why3 |
| 2 (Function) | Tip.Pretty.Isabelle |
| ppUninterp | |
| 1 (Function) | Tip.Pretty.SMT |
| 2 (Function) | Tip.Pretty.Why3 |
| 3 (Function) | Tip.Pretty.Isabelle |
| 4 (Function) | Tip.Pretty.TFF |
| ppUnqual | Tip.Pretty.Haskell |
| PPVar | |
| 1 (Type/Class) | Tip.Pretty |
| 2 (Data Constructor) | Tip.Pretty |
| ppVar | Tip.Pretty |
| prelude | Tip.Haskell.Translate |
| Pretty | Tip.Pretty |
| PrettyHsVar | Tip.Pretty.Haskell |
| PrettyVar | Tip.Pretty |
| projAt | Tip.Core |
| Projection | Tip.Types, Tip.Core |
| projector | Tip.Core |
| ProjectorInfo | Tip.Scope |
| projGlobal | Tip.Core |
| Prove | Tip.Types, Tip.Core |
| ProvedConjecture | Tip.Passes |
| provedConjecture | Tip.Passes |
| Qualified | Tip.Haskell.Translate |
| QualImport | Tip.Haskell.Repr |
| qual_func | Tip.Haskell.Translate |
| qual_module | Tip.Haskell.Translate |
| qual_module_short | Tip.Haskell.Translate |
| Quant | |
| 1 (Type/Class) | Tip.Types, Tip.Core |
| 2 (Data Constructor) | Tip.Types, Tip.Core |
| QuantIH | Tip.Types, Tip.Core |
| QuantInfo | Tip.Types, Tip.Core |
| QuickCheck | Tip.Haskell.Translate, Tip.Pretty.Haskell |
| quickCheck | Tip.Haskell.Translate |
| quickCheckAll | Tip.Haskell.Translate |
| quickCheckUnsafe | Tip.Haskell.Translate |
| QuickSpec | Tip.Haskell.Translate, Tip.Pretty.Haskell |
| quickSpec | Tip.Haskell.Translate |
| quote | Tip.Pretty.Isabelle |
| QuoteName | Tip.Haskell.Repr |
| QuoteTyCon | Tip.Haskell.Repr |
| quoteWhen | Tip.Pretty.Isabelle |
| Rec | Tip.Utils |
| Record | Tip.Haskell.Repr |
| recursive | Tip.Utils |
| refresh | Tip.Fresh |
| refreshLocal | Tip.Core |
| refreshNamed | Tip.Fresh |
| RemoveAliases | Tip.Passes |
| removeAliases | Tip.Passes |
| RemoveBuiltinBool | Tip.Passes |
| removeBuiltinBool | Tip.Pass.Booleans, Tip.Passes |
| removeBuiltinBoolFrom | Tip.Pass.Booleans |
| removeBuiltinBoolWith | Tip.Pass.Booleans |
| RemoveMatch | Tip.Passes |
| removeMatch | Tip.Passes |
| RemoveNewtype | Tip.Passes |
| removeNewtype | Tip.Passes |
| remove_variable_scrutinee_in_branches | Tip.Simplify, Tip.Passes |
| rename | Tip.Utils.Rename |
| renameAvoiding | Tip.Rename |
| renameDecls | Tip.Haskell.Rename |
| RenamedId | |
| 1 (Type/Class) | Tip.Rename |
| 2 (Data Constructor) | Tip.Rename |
| RenameM | Tip.Utils.Rename |
| RenameMap | Tip.Haskell.Rename, Tip.Pretty.Haskell |
| renameWith | Tip.Utils.Rename |
| renameWithBlocks | Tip.Utils.Rename |
| Role | Tip.Types, Tip.Core |
| Rule | |
| 1 (Type/Class) | Tip.Utils.Specialiser |
| 2 (Data Constructor) | Tip.Utils.Specialiser |
| rule_post | Tip.Utils.Specialiser |
| rule_pre | Tip.Utils.Specialiser |
| runFresh | Tip.Fresh |
| runFreshFrom | Tip.Fresh |
| runPass | Tip.Passes |
| runPasses | Tip.Passes |
| runPassLinted | Tip.Passes |
| runRenameM | Tip.Utils.Rename |
| runScope | Tip.Scope |
| runScopeT | Tip.Scope |
| runWriterT | Tip.Writer |
| safeRule | Tip.Utils.Specialiser |
| Scope | |
| 1 (Type/Class) | Tip.Scope |
| 2 (Data Constructor) | Tip.Scope |
| scope | Tip.Scope |
| ScopeM | Tip.Scope |
| ScopeT | |
| 1 (Type/Class) | Tip.Scope |
| 2 (Data Constructor) | Tip.Scope |
| Second | Tip.Passes |
| SelectConjecture | Tip.Passes |
| selectConjecture | Tip.Passes |
| separating | |
| 1 (Function) | Tip.Pretty.Why3 |
| 2 (Function) | Tip.Pretty.Isabelle |
| should_inline | Tip.Simplify, Tip.Passes |
| SigDecl | Tip.Types, Tip.Core |
| Signature | |
| 1 (Type/Class) | Tip.Types, Tip.Core |
| 2 (Data Constructor) | Tip.Types, Tip.Core |
| signature | Tip.Core |
| sig_name | Tip.Types, Tip.Core |
| sig_type | Tip.Types, Tip.Core |
| SimplifyAggressively | Tip.Passes |
| simplifyExpr | Tip.Simplify |
| simplifyExprIn | Tip.Simplify |
| SimplifyGently | Tip.Passes |
| SimplifyOpts | |
| 1 (Type/Class) | Tip.Simplify, Tip.Passes |
| 2 (Data Constructor) | Tip.Simplify, Tip.Passes |
| simplifyTheory | Tip.Simplify, Tip.Passes |
| skolemise | Tip.Passes |
| SkolemiseConjecture | Tip.Passes |
| skolemiseConjecture | Tip.Passes |
| skolemiseConjecture' | Tip.Passes |
| Smten | Tip.Haskell.Translate, Tip.Pretty.Haskell |
| smtenEnv | Tip.Haskell.Translate |
| smtenMinisat | Tip.Haskell.Translate |
| smtenMonad | Tip.Haskell.Translate |
| smtenSym | Tip.Haskell.Translate |
| smtKeywords | Tip.Pretty.SMT |
| Sort | |
| 1 (Type/Class) | Tip.Types, Tip.Core |
| 2 (Data Constructor) | Tip.Types, Tip.Core |
| SortDecl | Tip.Types, Tip.Core |
| SortInfo | Tip.Scope |
| SortsToNat | Tip.Passes |
| sortsToNat | Tip.Passes |
| sortThings | Tip.Utils |
| sort_name | Tip.Types, Tip.Core |
| sort_tvs | Tip.Types, Tip.Core |
| specialise | Tip.Utils.Specialiser |
| SplitConjecture | Tip.Passes |
| splitConjecture | Tip.Passes |
| StandardPass | Tip.Passes |
| Stmt | |
| 1 (Type/Class) | Tip.Haskell.Repr |
| 2 (Data Constructor) | Tip.Haskell.Repr |
| String | |
| 1 (Data Constructor) | Tip.Haskell.Repr |
| 2 (Data Constructor) | Tip.Types, Tip.Core |
| Subst | Tip.Utils.Specialiser |
| substMany | Tip.Core |
| subtermRules | Tip.Utils.Specialiser |
| subterms | Tip.Utils.Specialiser |
| Suggestor | Tip.Utils.Rename |
| sysEnv | Tip.Haskell.Translate |
| tell | Tip.Writer |
| tffify | Tip.Pretty.TFF |
| tffvarify | Tip.Pretty.TFF |
| TH | Tip.Haskell.Repr |
| Theory | |
| 1 (Type/Class) | Tip.Types, Tip.Core |
| 2 (Data Constructor) | Tip.Types, Tip.Core |
| theoryBoolOpToIf | Tip.Pass.Booleans, Tip.Passes |
| theoryBuiltins | Tip.Haskell.Translate |
| theoryDecls | Tip.Types, Tip.Core |
| theoryGoals | Tip.Core |
| theorySigs | Tip.Haskell.Translate |
| theoryStuff | Tip.CallGraph |
| theoryTypes | Tip.Core |
| THSplice | Tip.Haskell.Repr |
| thy_asserts | Tip.Types, Tip.Core |
| thy_datatypes | Tip.Types, Tip.Core |
| thy_funcs | Tip.Types, Tip.Core |
| thy_sigs | Tip.Types, Tip.Core |
| thy_sorts | Tip.Types, Tip.Core |
| tipDSL | Tip.Haskell.Translate |
| topsort | Tip.Core |
| touch_lets | Tip.Simplify, Tip.Passes |
| transformExpr | Tip.Types, Tip.Core |
| transformExprIn | Tip.Types, Tip.Core |
| transformExprInM | Tip.Types, Tip.Core |
| transformExprM | Tip.Types, Tip.Core |
| transformType | Tip.Types, Tip.Core |
| transformTypeInDecl | Tip.Types, Tip.Core |
| transformTypeInExpr | Tip.Types, Tip.Core |
| trBuiltinType | Tip.Haskell.Translate |
| trTheory | Tip.Haskell.Translate |
| trTheory' | Tip.Haskell.Translate |
| trType | Tip.Haskell.Translate |
| trueExpr | Tip.Core |
| trueName | Tip.Pass.Booleans |
| tryMatch | Tip.Simplify |
| Tup | Tip.Haskell.Repr |
| tuple | Tip.Pretty.Haskell |
| TupPat | Tip.Haskell.Repr |
| TyArr | Tip.Haskell.Repr |
| TyCon | |
| 1 (Data Constructor) | Tip.Haskell.Repr |
| 2 (Data Constructor) | Tip.Types, Tip.Core |
| TyCtx | Tip.Haskell.Repr |
| TyForall | Tip.Haskell.Repr |
| TyImp | Tip.Haskell.Repr |
| Type | |
| 1 (Type/Class) | Tip.Haskell.Repr |
| 2 (Type/Class) | Tip.Types, Tip.Core |
| typeable | Tip.Haskell.Translate |
| TypeDef | Tip.Haskell.Repr |
| TypeInfo | Tip.Scope |
| typeOfBuiltin | Tip.Haskell.Translate |
| types | Tip.Scope |
| TypeSkolemConjecture | Tip.Passes |
| typeSkolemConjecture | Tip.Passes |
| TySig | Tip.Haskell.Repr |
| TyTup | Tip.Haskell.Repr |
| TyVar | |
| 1 (Data Constructor) | Tip.Haskell.Repr |
| 2 (Data Constructor) | Tip.Types, Tip.Core |
| TyVarInfo | Tip.Scope |
| tyVars | Tip.Core |
| ufInfo | Tip.Haskell.Translate |
| UncurryTheory | Tip.Passes |
| uncurryTheory | Tip.Passes |
| unionOn | Tip.Utils |
| UniqLocals | Tip.Passes |
| uniqLocals | Tip.Passes |
| unitPass | Tip.Passes |
| Unknown | Tip.Types, Tip.Core |
| unPPVar | Tip.Pretty |
| unsafeSubst | Tip.Core |
| unScopeT | Tip.Scope |
| unWriterT | Tip.Writer |
| updateFuncType | Tip.Core |
| updateLocalType | Tip.Core |
| UserAsserted | Tip.Types, Tip.Core |
| uses | Tip.Core |
| usort | Tip.Utils |
| usortOn | Tip.Utils |
| validChar | Tip.Pretty.Waldmeister |
| validSMTChar | Tip.Pretty.SMT |
| validTFFChar | Tip.Pretty.TFF |
| Var | Tip.Utils.Specialiser |
| var | Tip.Haskell.Repr |
| VarPat | Tip.Haskell.Repr |
| varStr | Tip.Pretty |
| varUnqual | Tip.Pretty.Haskell |
| Void | Tip.Utils.Specialiser |
| Where | Tip.Haskell.Repr |
| whichConstructor | Tip.Scope |
| whichDatatype | Tip.Scope |
| whichDiscriminator | Tip.Scope |
| whichFunction | Tip.Scope |
| whichGlobal | Tip.Scope |
| whichLocal | Tip.Scope |
| whichProjector | Tip.Scope |
| why3Keywords | Tip.Pretty.Why3 |
| Why3Var | |
| 1 (Type/Class) | Tip.Pretty.Why3 |
| 2 (Data Constructor) | Tip.Pretty.Why3 |
| why3VarTheory | Tip.Pretty.Why3 |
| WildPat | Tip.Haskell.Repr |
| withBool | Tip.Haskell.Translate |
| withPrevious | Tip.Utils |
| withTheory | Tip.Scope |
| WorkerWrapper | |
| 1 (Type/Class) | Tip.WorkerWrapper |
| 2 (Data Constructor) | Tip.WorkerWrapper |
| workerWrapper | Tip.WorkerWrapper |
| workerWrapperFunctions | Tip.WorkerWrapper |
| workerWrapperTheory | Tip.WorkerWrapper |
| WriterT | |
| 1 (Type/Class) | Tip.Writer |
| 2 (Data Constructor) | Tip.Writer |
| ww_args | Tip.WorkerWrapper |
| ww_def | Tip.WorkerWrapper |
| ww_func | Tip.WorkerWrapper |
| ww_res | Tip.WorkerWrapper |
| ww_use | Tip.WorkerWrapper |
| \/ | Tip.Core |