• register
  • log in

hub.darcs.net :: dolio -> agda-share -> files

random agda experiments

root

  • categorica
  • cubical
  • halting
  • hoas
  • induction
  • injective
  • logic
  • lrs
  • nbe
  • sorting
  • universes
  • why-not-w
  • .boring
  • AVL.agda
  • AckInd0.agda
  • BijectiveIso.agda
  • Bindings.agda
  • CExp.agda
  • CI.agda
  • ChurchLaw.agda
  • Coexp.agda
  • Conat.agda
  • ContAdj.agda
  • Coprod.agda
  • Countable.agda
  • DC.agda
  • DecEq.agda
  • DepCat.agda
  • DiaFun.agda
  • Diag.agda
  • Distinct.agda
  • EckmannHilton.agda
  • ExistentialCoinduction.agda
  • F.agda
  • Fib.agda
  • FibredImpredicative.agda
  • FinLT.agda
  • FinalAlgebra.agda
  • Float.agda
  • Foundation.agda
  • Free.agda
  • FunView.agda
  • HEqExt.agda
  • Horse.agda
  • IOE.agda
  • IRDomain.agda
  • IRHurkens.agda
  • IRSetTheory.agda
  • IndexedMonad.agda
  • Infinitary.agda
  • Infinite.agda
  • InfiniteDescent.agda
  • InjTCSplit.agda
  • Interp.agda
  • K.agda
  • Kripke.agda
  • LICENCE
  • Lenses.agda
  • MFin.agda
  • MuNu.agda
  • Negative.agda
  • Nest.agda
  • NestPoly.agda
  • Newtype.agda
  • Ordinal.agda
  • PHOASNorm.agda
  • PW.agda
  • ParamFunc.agda
  • ParamInduction.agda
  • ParamProj.agda
  • ParametricTerminal.agda
  • Pent.agda
  • Pigeon.agda
  • Prime.agda
  • PropRewrite.agda
  • PushoutQuotients.agda
  • QuickSort.agda
  • Rat.agda
  • Refinement.agda
  • Regular.agda
  • Russell.agda
  • SKI.agda
  • SetoidFacts.agda
  • SetoidPushout.agda
  • StateAlgebra.agda
  • TrivMLTT.agda
  • Two.agda
  • WISC.agda
  • WeirdSetoid.agda
  • WhyNotW.agda
  • ZigZag.agda
  • Zip.agda
  • agda-share.agda-lib
  • files
  • changes
  • fork
  • download .zip
  • darcs get url
  • darcsden 1.2 beta built Jun 23 201810:48:19
  • report problems to simon