above | FreeC.IR.Subterm |
Abstract | FreeC.Backend.Agda.Syntax |
AbstractDef | FreeC.Backend.Agda.Syntax |
abstractTypeScheme | FreeC.IR.TypeScheme |
abstractTypeScheme' | FreeC.IR.TypeScheme |
Absurd | FreeC.Backend.Agda.Syntax |
AbsurdLam | FreeC.Backend.Agda.Syntax |
AbsurdP | FreeC.Backend.Agda.Syntax |
AbsurdRHS | FreeC.Backend.Agda.Syntax |
Access | FreeC.Backend.Agda.Syntax |
access | FreeC.Backend.Coq.Syntax |
AccessIdent | FreeC.Backend.Coq.Syntax |
addCohesion | FreeC.Backend.Agda.Syntax |
addEffectsToEntry | FreeC.Environment |
addEntry | FreeC.Environment |
addFreeArgs | FreeC.Backend.Agda.Converter.Free |
addModality | FreeC.Backend.Agda.Syntax |
addPartial | FreeC.Backend.Agda.Converter.Free |
addQuantity | FreeC.Backend.Agda.Syntax |
addRelevance | FreeC.Backend.Agda.Syntax |
AgdaFileType | FreeC.Backend.Agda.Syntax |
agdaKeywords | FreeC.Backend.Agda.Keywords |
align | FreeC.Pretty |
allCohesions | FreeC.Backend.Agda.Syntax |
allPos | FreeC.IR.Subterm |
allRelevances | FreeC.Backend.Agda.Syntax |
Alt | |
1 (Type/Class) | FreeC.IR.Syntax.Expr, FreeC.IR.Syntax |
2 (Data Constructor) | FreeC.IR.Syntax.Expr, FreeC.IR.Syntax |
3 (Type/Class) | FreeC.LiftedIR.Syntax.Expr, FreeC.LiftedIR.Syntax |
4 (Data Constructor) | FreeC.LiftedIR.Syntax.Expr, FreeC.LiftedIR.Syntax |
altConPat | |
1 (Function) | FreeC.IR.Syntax.Expr, FreeC.IR.Syntax |
2 (Function) | FreeC.LiftedIR.Syntax.Expr, FreeC.LiftedIR.Syntax |
altRhs | |
1 (Function) | FreeC.IR.Syntax.Expr, FreeC.IR.Syntax |
2 (Function) | FreeC.LiftedIR.Syntax.Expr, FreeC.LiftedIR.Syntax |
altSrcSpan | |
1 (Function) | FreeC.IR.Syntax.Expr, FreeC.IR.Syntax |
2 (Function) | FreeC.LiftedIR.Syntax.Expr, FreeC.LiftedIR.Syntax |
altVarPats | |
1 (Function) | FreeC.IR.Syntax.Expr, FreeC.IR.Syntax |
2 (Function) | FreeC.LiftedIR.Syntax.Expr, FreeC.LiftedIR.Syntax |
ancestorPos | FreeC.IR.Subterm |
angles | FreeC.Pretty |
AnyIsAbstract | FreeC.Backend.Agda.Syntax |
anyIsAbstract | FreeC.Backend.Agda.Syntax |
AnyWhere | FreeC.Backend.Agda.Syntax |
App | |
1 (Data Constructor) | FreeC.Backend.Coq.Syntax |
2 (Data Constructor) | FreeC.IR.Syntax.Expr, FreeC.IR.Syntax |
3 (Data Constructor) | FreeC.Backend.Agda.Syntax |
4 (Data Constructor) | FreeC.LiftedIR.Syntax.Expr, FreeC.LiftedIR.Syntax |
app | |
1 (Function) | FreeC.Backend.Coq.Syntax |
2 (Function) | FreeC.IR.Syntax.Expr, FreeC.IR.Syntax |
3 (Function) | FreeC.Backend.Agda.Syntax |
appendArgNames | FreeC.Backend.Agda.Syntax |
applyCohesion | FreeC.Backend.Agda.Syntax |
applyFreeArgs | FreeC.Backend.Agda.Converter.Free |
applyModality | FreeC.Backend.Agda.Syntax |
applyQuantity | FreeC.Backend.Agda.Syntax |
applyRelevance | FreeC.Backend.Agda.Syntax |
ApplySubst | FreeC.IR.Subst |
applySubst | FreeC.IR.Subst |
appN | FreeC.Backend.Agda.Syntax |
AppP | FreeC.Backend.Agda.Syntax |
appP | FreeC.Backend.Agda.Syntax |
AppView | |
1 (Type/Class) | FreeC.Backend.Agda.Syntax |
2 (Data Constructor) | FreeC.Backend.Agda.Syntax |
appView | FreeC.Backend.Agda.Syntax |
Arg | |
1 (Type/Class) | FreeC.Backend.Coq.Syntax |
2 (Type/Class) | FreeC.Backend.Agda.Syntax |
3 (Data Constructor) | FreeC.Backend.Agda.Syntax |
ArgExplicit | FreeC.Backend.Coq.Syntax |
ArgImplicit | FreeC.Backend.Coq.Syntax |
ArgInfo | |
1 (Type/Class) | FreeC.Backend.Agda.Syntax |
2 (Data Constructor) | FreeC.Backend.Agda.Syntax |
argInfo | FreeC.Backend.Agda.Syntax |
argInfoFreeVariables | FreeC.Backend.Agda.Syntax |
argInfoHiding | FreeC.Backend.Agda.Syntax |
argInfoModality | FreeC.Backend.Agda.Syntax |
argInfoOrigin | FreeC.Backend.Agda.Syntax |
ArgMaximal | FreeC.Backend.Coq.Syntax |
ArgName | FreeC.Backend.Agda.Syntax |
argNameToString | FreeC.Backend.Agda.Syntax |
ArgsPat | FreeC.Backend.Coq.Syntax |
ArgumentExplicitness | FreeC.Backend.Coq.Syntax |
Arguments | |
1 (Type/Class) | FreeC.Backend.Coq.Syntax |
2 (Data Constructor) | FreeC.Backend.Coq.Syntax |
ArgumentSpec | |
1 (Type/Class) | FreeC.Backend.Coq.Syntax |
2 (Data Constructor) | FreeC.Backend.Coq.Syntax |
ArgumentsSentence | FreeC.Backend.Coq.Syntax |
Arity | FreeC.Backend.Agda.Syntax |
Arrow | FreeC.Backend.Coq.Syntax |
arrows | FreeC.Backend.Coq.Syntax |
As | FreeC.Backend.Agda.Syntax |
AsName | |
1 (Type/Class) | FreeC.Backend.Agda.Syntax |
2 (Data Constructor) | FreeC.Backend.Agda.Syntax |
asName | FreeC.Backend.Agda.Syntax |
AsName' | FreeC.Backend.Agda.Syntax |
AsP | FreeC.Backend.Agda.Syntax |
AsPat | FreeC.Backend.Coq.Syntax |
asRange | FreeC.Backend.Agda.Syntax |
Assertion | |
1 (Type/Class) | FreeC.Backend.Coq.Syntax |
2 (Data Constructor) | FreeC.Backend.Coq.Syntax |
AssertionKeyword | FreeC.Backend.Coq.Syntax |
AssertionSentence | FreeC.Backend.Coq.Syntax |
Associativity | |
1 (Type/Class) | FreeC.Backend.Coq.Syntax |
2 (Type/Class) | FreeC.Backend.Agda.Syntax |
Assumption | |
1 (Type/Class) | FreeC.Backend.Coq.Syntax |
2 (Data Constructor) | FreeC.Backend.Coq.Syntax |
AssumptionKeyword | FreeC.Backend.Coq.Syntax |
AssumptionSentence | FreeC.Backend.Coq.Syntax |
Assums | |
1 (Type/Class) | FreeC.Backend.Coq.Syntax |
2 (Data Constructor) | FreeC.Backend.Coq.Syntax |
At | FreeC.Frontend.IR.Token |
Axiom | FreeC.Backend.Coq.Syntax |
Axioms | FreeC.Backend.Coq.Syntax |