• Home
• Search 
• Browse
• What's new
• Upload
• User accounts

Directory listing for Agda-2.6.4.3 source tarball

Agda-2.6.4.3/src/full/Agda/TypeChecking/

• Abstract.hs
• CheckInternal.hs
• CheckInternal.hs-boot
• CompiledClause.hs
• Constraints.hs
• Constraints.hs-boot
• Conversion.hs
• Conversion.hs-boot
• Coverage.hs
• Datatypes.hs
• Datatypes.hs-boot
• DeadCode.hs
• DisplayForm.hs
• DropArgs.hs
• Empty.hs
• Empty.hs-boot
• Errors.hs
• Errors.hs-boot
• EtaContract.hs
• Forcing.hs
• Free.hs
• Functions.hs
• Generalize.hs
• IApplyConfluence.hs
• Implicit.hs
• Injectivity.hs
• Inlining.hs
• InstanceArguments.hs
• Irrelevance.hs
• Irrelevance.hs-boot
• Level.hs
• Level.hs-boot
• LevelConstraints.hs
• Lock.hs
• Lock.hs-boot
• MetaVars.hs
• MetaVars.hs-boot
• Modalities.hs
• Monad.hs
• Names.hs
• Opacity.hs
• Opacity.hs-boot
• Polarity.hs
• Polarity.hs-boot
• Positivity.hs
• Pretty.hs
• Pretty.hs-boot
• Primitive.hs
• Primitive.hs-boot
• ProjectionLike.hs
• ProjectionLike.hs-boot
• Quote.hs
• ReconstructParameters.hs
• RecordPatterns.hs
• Records.hs
• Records.hs-boot
• Reduce.hs
• Reduce.hs-boot
• Rewriting.hs
• Rewriting.hs-boot
• Serialise.hs
• SizedTypes.hs
• Sort.hs
• Substitute.hs
• SyntacticEquality.hs
• Telescope.hs
• Telescope.hs-boot
• Unquote.hs
• Warnings.hs
• With.hs
• CompiledClause/
  • Compile.hs
  • Compile.hs-boot
  • Match.hs
  • Match.hs-boot
• Conversion/
  • Pure.hs
• Coverage/
  • Cubical.hs
  • Match.hs
  • SplitClause.hs
  • SplitTree.hs
• Free/
  • Lazy.hs
  • Precompute.hs
  • Reduce.hs
• Level/
  • Solve.hs
• MetaVars/
  • Mention.hs
  • Occurs.hs
• Monad/
  • Base.hs
  • Base.hs-boot
  • Benchmark.hs
  • Builtin.hs
  • Builtin.hs-boot
  • Caching.hs
  • Closure.hs
  • Constraints.hs
  • Context.hs
  • Context.hs-boot
  • Debug.hs
  • Debug.hs-boot
  • Env.hs
  • Imports.hs
  • MetaVars.hs
  • MetaVars.hs-boot
  • Modality.hs
  • Mutual.hs
  • Open.hs
  • Options.hs
  • Options.hs-boot
  • Pure.hs
  • Pure.hs-boot
  • Signature.hs
  • Signature.hs-boot
  • SizedTypes.hs
  • State.hs
  • Statistics.hs
  • Trace.hs
  • Base/
    • Warning.hs
• Patterns/
  • Abstract.hs
  • Internal.hs
  • Match.hs
  • Match.hs-boot
• Positivity/
  • Occurrence.hs
• Pretty/
  • Call.hs
  • Call.hs-boot
  • Constraint.hs
  • Constraint.hs-boot
  • Warning.hs
  • Warning.hs-boot
• Primitive/
  • Base.hs
  • Cubical.hs
  • Cubical/
    • Base.hs
    • Base.hs-boot
    • Glue.hs
    • HCompU.hs
    • Id.hs
• Reduce/
  • Fast.hs
  • Fast.hs-boot
  • Monad.hs
• Rewriting/
  • Clause.hs
  • Confluence.hs
  • NonLinMatch.hs
  • NonLinPattern.hs
• Rules/
  • Application.hs
  • Application.hs-boot
  • Builtin.hs
  • Data.hs
  • Data.hs-boot
  • Decl.hs
  • Decl.hs-boot
  • Def.hs
  • Def.hs-boot
  • Display.hs
  • LHS.hs
  • Record.hs
  • Term.hs
  • Term.hs-boot
  • Builtin/
    • Coinduction.hs
    • Coinduction.hs-boot
  • LHS/
    • Implicit.hs
    • Problem.hs
    • ProblemRest.hs
    • Unify.hs
    • Unify/
      • LeftInverse.hs
      • Types.hs
• Serialise/
  • Base.hs
  • Instances.hs
  • Instances/
    • Abstract.hs
    • Common.hs
    • Compilers.hs
    • Errors.hs
    • Highlighting.hs
    • Internal.hs
• SizedTypes/
  • Solve.hs
  • Syntax.hs
  • Utils.hs
  • WarshallSolver.hs
• Substitute/
  • Class.hs
  • DeBruijn.hs
• Telescope/
  • Path.hs