Skip to content

Instantly share code, notes, and snippets.

@dellamora

dellamora/poggers.md

Created October 2, 2024 20:00
Show Gist options
  • Save dellamora/65c916ada6de0bcf182103211b92c7c7 to your computer and use it in GitHub Desktop.
Save dellamora/65c916ada6de0bcf182103211b92c7c7 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
poggers.md

ARC/DSL/Functions/

0/

  • add.agda
  • apply.agda
  • compose.agda
  • container-to-list.agda
  • dedupe.agda
  • equality.agda
  • first.agda
  • greater.agda
  • int-cmp.agda
  • leastcommon.agda
  • merge.agda
  • mostcommon.agda
  • papply.agda
  • remove.agda
  • sfilter.agda
  • size.agda
  • subtract.agda
  • tolist.agda

ARC/DSL/Types/Boolean/

0/

  • Boolean.agda
  • Functions.agda

ARC/DSL/Types/Cell/

0/

  • Cell.agda

ARC/DSL/Types/Container/

0/

  • Container.agda
  • Functions.agda

ARC/DSL/Types/Element/

0/

  • Element.agda

ARC/DSL/Types/Grid/

0/

  • Grid.agda

ARC/DSL/Types/Indices/

0/

  • Indices.agda

ARC/DSL/Types/Integer/

0/

  • Functions.agda
  • Integer.agda

ARC/DSL/Types/IntegerList/

0/

  • IntegerList.agda

ARC/DSL/Types/IntegerSet/

0/

  • IntegerSet.agda

ARC/DSL/Types/List/

0/

  • Functions.agda
  • List.agda

ARC/DSL/Types/Numerical/

0/

  • Numerical.agda

ARC/DSL/Types/Object/

0/

  • Object.agda

ARC/DSL/Types/OrdSet/

0/

  • Functions.agda
  • OrdSet.agda

ARC/DSL/Types/Pair/

0/

  • Functions.agda
  • Pair.agda

ARC/DSL/Types/Patch/

0/

  • Patch.agda

ARC/DSL/Types/Piece/

0/

  • Piece.agda

ARC/DSL/Types/Union/

0/

  • Union.agda

Base/

0/

  • ALL.agda

Base/AVLTree/

0/

  • ALL.agda
  • AVLTree.agda
  • delete.agda
  • difference.agda
  • empty.agda
  • filter.agda
  • fold.agda
  • from-list.agda
  • get-pair.agda
  • get.agda
  • has-key.agda
  • height.agda
  • insert.agda
  • intersect.agda
  • invert.agda
  • is-balanced.agda
  • keys.agda
  • map-keys.agda
  • map-values.agda
  • map.agda
  • maximum.agda
  • minimum.agda
  • singleton.agda
  • size.agda
  • to-list.agda
  • union.agda
  • values.agda

Base/AVLTree/Balance/

0/

  • Balance.agda
  • eq.agda
  • neq.agda
  • rotate-left.agda
  • rotate-right.agda

Base/AVLTree/Balance/Trait/

0/

  • Eq.agda

Base/AVLTree/Delete/

0/

  • delete-go.agda
  • delete-maximum.agda

Base/BinTree/

0/

  • ALL.agda
  • BinTree.agda
  • all-equal.agda
  • count.agda
  • eq.agda
  • fold.agda
  • merge.agda
  • neq.agda
  • show.agda
  • sum.agda

Base/BinTree/Trait/

0/

  • Eq.agda
  • Show.agda

Base/BitMap/

0/

  • ALL.agda
  • BitMap.agda
  • contains.agda
  • count.agda
  • del.agda
  • difference.agda
  • empty.agda
  • from-list.agda
  • get.agda
  • insert.agda
  • merge.agda
  • new.agda
  • set.agda
  • show.agda
  • swap.agda
  • take.agda
  • to-list.agda
  • union.agda
  • values.agda

Base/BitMap/Tm/

0/

  • get-set.agda

Base/BitMap/Trait/

0/

  • Show.agda

Base/Bits/

0/

  • ALL.agda
  • Bits.agda
  • add.agda
  • and.agda
  • append.agda
  • compare.agda
  • concat.agda
  • dec.agda
  • decode-utf8.agda
  • div.agda
  • encode-char-utf8.agda
  • encode-utf8.agda
  • eq.agda
  • from-char.agda
  • from-nat.agda
  • gt.agda
  • gte.agda
  • inc.agda
  • is-zero.agda
  • length.agda
  • lshift.agda
  • lt.agda
  • lte.agda
  • mod.agda
  • mul.agda
  • neq.agda
  • normal.agda
  • not.agda
  • or.agda
  • pad-length.agda
  • pad-zeros.agda
  • pred.agda
  • reverse.agda
  • rshift.agda
  • show-rev.agda
  • show.agda
  • split-at.agda
  • split-chunks.agda
  • sub.agda
  • succ.agda
  • take.agda
  • to-char.agda
  • to-nat.agda
  • xor.agda

Base/Bits/Decode-utf8/

0/

  • decode-utf8-go.agda

Base/Bits/Trait/

0/

  • Eq.agda
  • Ord.agda
  • Show.agda

Base/Bool/

0/

  • ALL.agda
  • Bool.agda
  • and.agda
  • eq.agda
  • if.agda
  • neq.agda
  • not.agda
  • or.agda
  • show.agda
  • xor.agda

Base/Bool/Trait/

0/

  • Eq.agda
  • Show.agda

Base/Buffer/

0/

  • ALL.agda
  • Buffer.agda
  • get.agda
  • new.agda
  • set.agda

Base/ByteString/

0/

  • ALL.agda
  • ByteString.agda
  • append.agda
  • concat.agda
  • cons.agda
  • drop.agda
  • head.agda
  • is-empty.agda
  • pack-string-fixed.agda
  • pack-string.agda
  • pack.agda
  • read-char.agda
  • read-f64.agda
  • read-u48.agda
  • show.agda
  • slice.agda
  • tail.agda
  • take.agda
  • unpack.agda
  • write-f64-as-nat.agda
  • write-u48.agda

Base/ByteString/Trait/

0/

  • Show.agda

Base/Char/

0/

  • ALL.agda
  • Char.agda
  • compare.agda
  • digit-to-nat.agda
  • eq.agda
  • from-nat.agda
  • gt.agda
  • gte.agda
  • hex-to-nat.agda
  • is-alpha.agda
  • is-ascii.agda
  • is-digit.agda
  • is-hex-digit.agda
  • is-latin1.agda
  • is-lower.agda
  • is-print.agda
  • is-space.agda
  • lt.agda
  • lte.agda
  • neq.agda
  • show.agda
  • to-digit.agda
  • to-lower.agda
  • to-nat.agda
  • to-upper.agda

Base/Char/Trait/

0/

  • Eq.agda
  • Ord.agda
  • Show.agda

Base/Concurrent/Channel/

0/

  • Channel.agda
  • new.agda
  • read.agda
  • write.agda

Base/DiffList/

0/

  • ALL.agda
  • DiffList.agda
  • append.agda
  • cons.agda
  • empty.agda
  • snoc.agda
  • to-list.agda

Base/Either/

0/

  • ALL.agda
  • Either.agda

Base/Empty/

0/

  • ALL.agda
  • Empty.agda

Base/Equal/

0/

  • ALL.agda
  • Equal.agda
  • apply.agda
  • erase.agda
  • left.agda
  • right.agda
  • subst.agda
  • sym.agda
  • trans.agda

Base/F64/

0/

  • ALL.agda
  • F64.agda
  • acos.agda
  • add.agda
  • and.agda
  • asin.agda
  • atan.agda
  • compare.agda
  • cos.agda
  • cosh.agda
  • div.agda
  • double.agda
  • eq.agda
  • exp.agda
  • floor.agda
  • from-bits.agda
  • from-int.agda
  • from-nat.agda
  • from-string.agda
  • from-u64.agda
  • gt.agda
  • gte.agda
  • half.agda
  • log.agda
  • lt.agda
  • lte.agda
  • max.agda
  • min.agda
  • mod.agda
  • mul.agda
  • negate.agda
  • neq.agda
  • or.agda
  • show.agda
  • sin.agda
  • sinh.agda
  • sqrt.agda
  • square.agda
  • sub.agda
  • tan.agda
  • tanh.agda
  • to-bits.agda
  • to-u64.agda

Base/F64/Trait/

0/

  • Eq.agda
  • Ord.agda
  • Show.agda

Base/Function/

0/

  • ALL.agda
  • case.agda
  • const.agda
  • id.agda

Base/IO/

0/

  • ALL.agda
  • IO.agda
  • append-file.agda
  • delete-file.agda
  • exists.agda
  • get-args.agda
  • get-line.agda
  • is-directory.agda
  • is-file.agda
  • mkdir.agda
  • print.agda
  • read-file.agda
  • write-file.agda

Base/IO/Monad/

0/

  • bind.agda
  • pure.agda

Base/IO/Trait/

0/

  • Monad.agda

Base/Int/

0/

  • ALL.agda
  • Int.agda
  • compare.agda
  • eq.agda
  • from-nat.agda
  • from-neg.agda
  • gt.agda
  • gte.agda
  • lt.agda
  • lte.agda
  • mul.agda
  • neg.agda
  • neq.agda
  • show.agda
  • to-bits.agda
  • to-nat.agda

Base/Int/Trait/

0/

  • Eq.agda
  • Ord.agda
  • Show.agda

Base/JSON/

0/

  • ALL.agda
  • JSON.agda
  • parse-array.agda
  • parse-bool.agda
  • parse-null.agda
  • parse-number.agda
  • parse-object.agda
  • parse-string.agda
  • parse.agda
  • show.agda

Base/JSON/Trait/

0/

  • Show.agda

Base/List/

0/

  • ALL.agda
  • List.agda
  • all-equal.agda
  • all-true.agda
  • and.agda
  • any-true.agda
  • append.agda
  • cartesian-product-with.agda
  • cartesian-product.agda
  • compare.agda
  • concat-map.agda
  • concat-maybes.agda
  • concat.agda
  • contains.agda
  • count.agda
  • dedup.agda
  • diagonal.agda
  • difference.agda
  • drop-while.agda
  • drop.agda
  • empty.agda
  • eq.agda
  • filter.agda
  • find.agda
  • foldl.agda
  • foldr.agda
  • frequency.agda
  • gt.agda
  • gte.agda
  • head.agda
  • inits.agda
  • insert-at-sorted.agda
  • insert-at.agda
  • insertion-sort.agda
  • intercalate.agda
  • intersperse.agda
  • is-asc.agda
  • is-cons.agda
  • is-nil.agda
  • iterate.agda
  • last.agda
  • length.agda
  • lookup.agda
  • lt.agda
  • lte.agda
  • map.agda
  • match.agda
  • mfoldl.agda
  • mmap.agda
  • neq.agda
  • or.agda
  • product.agda
  • quicksort.agda
  • remove-at.agda
  • replicate.agda
  • reverse.agda
  • show.agda
  • singleton.agda
  • sort.agda
  • split-at-element.agda
  • split-at.agda
  • split-chunks.agda
  • split-first.agda
  • split-last.agda
  • starts-with.agda
  • sum.agda
  • tail.agda
  • tails.agda
  • take-while.agda
  • take.agda
  • unsnoc.agda
  • unzip-with.agda
  • unzip.agda
  • update-at.agda
  • zip-cons.agda
  • zip-with.agda
  • zip.agda

Base/List/Monad/

0/

  • bind.agda
  • pure.agda

Base/List/Omega/

0/

  • Omega.agda

Base/List/Tm/

0/

  • is-cons.agda
  • is-nil.agda

Base/List/Trait/

0/

  • Eq.agda
  • Monad.agda
  • Ord.agda
  • Show.agda

Base/Maybe/

0/

  • ALL.agda
  • Maybe.agda
  • eq.agda
  • fold.agda
  • map.agda
  • neq.agda
  • run.agda
  • show.agda
  • to-bool.agda
  • to-list.agda
  • to-result.agda

Base/Maybe/Monad/

0/

  • bind.agda
  • pure.agda

Base/Maybe/Trait/

0/

  • Eq.agda
  • Monad.agda
  • Show.agda

Base/Nat/

0/

  • ALL.agda
  • Nat.agda
  • add.agda
  • compare.agda
  • div.agda
  • double.agda
  • eq.agda
  • exp.agda
  • gt.agda
  • gte.agda
  • half.agda
  • is-zero.agda
  • lt.agda
  • lte.agda
  • match.agda
  • max.agda
  • min.agda
  • mod.agda
  • mul.agda
  • neq.agda
  • pred.agda
  • range.agda
  • rshift.agda
  • show.agda
  • sub.agda
  • to-bits.agda
  • to-u64.agda
  • xor.agda

Base/Nat/Trait/

0/

  • Add.agda
  • Eq.agda
  • Ord.agda
  • Show.agda

Base/Nat/div/

0/

  • go.agda

Base/Network/HTTP/Method/

0/

  • Method.agda
  • to-string.agda

Base/Network/HTTP/

0/

  • fetch.agda

Base/Network/WebSocket/

0/

  • WSConnection.agda
  • receive-binary-data.agda
  • receive-data.agda
  • run-client.agda
  • run-concurrent-client.agda
  • run-secure-client.agda
  • send-binary-data.agda
  • send-close.agda
  • send-text-data.agda

Base/OrdMap/

0/

  • ALL.agda
  • OrdMap.agda
  • delete.agda
  • difference.agda
  • empty.agda
  • fold.agda
  • from-list.agda
  • get-pair.agda
  • get.agda
  • has-key.agda
  • insert.agda
  • intersect.agda
  • keys.agda
  • singleton.agda
  • to-list.agda
  • union.agda
  • values.agda

Base/OrdSet/

0/

  • ALL.agda
  • OrdSet.agda
  • contains.agda
  • delete.agda
  • difference.agda
  • empty.agda
  • filter.agda
  • fold.agda
  • from-list.agda
  • insert.agda
  • intersect.agda
  • map.agda
  • maximum.agda
  • minimum.agda
  • singleton.agda
  • size.agda
  • to-list.agda
  • union.agda

Base/Ordering/

0/

  • ALL.agda
  • Ordering.agda
  • eq.agda
  • neq.agda

Base/Ordering/Trait/

0/

  • Eq.agda

Base/Pair/

0/

  • ALL.agda
  • Pair.agda
  • eq.agda
  • get-fst.agda
  • get-snd.agda
  • map.agda
  • mut-fst.agda
  • mut-snd.agda
  • neq.agda
  • set-fst.agda
  • set-snd.agda
  • show.agda
  • to-list.agda

Base/Pair/Trait/

0/

  • Eq.agda
  • Show.agda

Base/Parser/

0/

  • ALL.agda
  • Error.agda
  • Parser.agda
  • Reply.agda
  • State.agda
  • advance-many.agda
  • advance-one.agda
  • alternative.agda
  • consume.agda
  • fail.agda
  • get-index.agda
  • is-eof.agda
  • map.agda
  • parse-char.agda
  • parse-many.agda
  • parse-name.agda
  • parse-quoted-char.agda
  • parse-string.agda
  • peek-many.agda
  • peek-one.agda
  • skip-spaces.agda
  • skip-trivia.agda
  • starts-with.agda
  • take-while.agda

Base/Parser/Examples/LambdaTerm/

0/

  • LambdaTerm.agda
  • new.agda
  • parse.agda

Base/Parser/Monad/

0/

  • bind.agda
  • pure.agda

Base/Queue/

0/

  • ALL.agda
  • Queue.agda
  • dequeue.agda
  • enqueue.agda

Base/Result/

0/

  • ALL.agda
  • Result.agda
  • fold.agda

Base/Result/Monad/

0/

  • bind.agda

Base/Result/Trait/

0/

  • Monad.agda

Base/String/

0/

  • ALL.agda
  • String.agda
  • append.agda
  • compare.agda
  • contains.agda
  • drop.agda
  • eq.agda
  • foldr.agda
  • from-char.agda
  • from-list.agda
  • gt.agda
  • gte.agda
  • hash.agda
  • head.agda
  • is-empty.agda
  • join.agda
  • length.agda
  • lt.agda
  • lte.agda
  • neq.agda
  • replicate.agda
  • show.agda
  • split-at.agda
  • starts-with.agda
  • to-list.agda
  • to-nat-base.agda
  • uncons.agda

Base/String/Trait/

0/

  • Eq.agda
  • Monoid.agda
  • Ord.agda
  • Show.agda

Base/Time/

0/

  • ALL.agda
  • now.agda

Base/Trait/

0/

  • ALL.agda
  • Add.agda
  • Eq.agda
  • Monad.agda
  • Monoid.agda
  • Ord.agda
  • Show.agda

Base/U64/

0/

  • ALL.agda
  • U64.agda
  • add.agda
  • and.agda
  • compare.agda
  • div.agda
  • double.agda
  • eq.agda
  • from-bits.agda
  • from-bool.agda
  • from-nat.agda
  • gt.agda
  • gte.agda
  • if.agda
  • lt.agda
  • lte.agda
  • max.agda
  • min.agda
  • mod.agda
  • mul.agda
  • neq.agda
  • not.agda
  • or.agda
  • show.agda
  • sub.agda
  • to-bits.agda
  • to-nat.agda
  • xor.agda

Base/U64/Trait/

0/

  • Eq.agda
  • Ord.agda
  • Show.agda

Base/Unit/

0/

  • ALL.agda
  • Unit.agda
  • eq.agda
  • neq.agda

Base/Unit/Trait/

0/

  • Eq.agda

Base/V2/

0/

  • ALL.agda
  • V2.agda
  • add.agda
  • dist.agda
  • div-scalar.agda
  • div.agda
  • dot.agda
  • eq.agda
  • length.agda
  • lerp.agda
  • max.agda
  • min.agda
  • mul-scalar.agda
  • negate.agda
  • neq.agda
  • normalize.agda
  • perpendicular.agda
  • show.agda
  • sqr-dist.agda
  • sub.agda

Base/V2/Trait/

0/

  • Eq.agda
  • Show.agda

Base/Word8/

0/

  • ALL.agda
  • Word8.agda
  • from-nat.agda
  • to-nat.agda

Bend/Cli/Command/

0/

  • Command.agda
  • from-string.agda

Bend/Compile/BendToNet/Encoder/

0/

  • Encoder.agda
  • encode-num.agda
  • encode-pat.agda
  • encode-term.agda
  • link-var.agda
  • link.agda
  • new-node.agda
  • new.agda

Bend/Compile/BendToNet/

0/

  • book-to-nets.agda

Bend/Compile/NetToHvm/State/

0/

  • State.agda
  • new.agda

Bend/Compile/NetToHvm/

0/

  • get-redexes.agda
  • net-to-hvm.agda
  • nets-to-hvm.agda
  • tree-to-hvm.agda

Bend/Compile/

0/

  • book-to-hvm.agda

Bend/Fun/Adt/

0/

  • Adt.agda
  • Ctr.agda
  • CtrField.agda

Bend/Fun/Book/

0/

  • Book.agda
  • add-fn-def.agda
  • contains-def.agda
  • get-adt.agda
  • get-ctr.agda
  • new.agda
  • show.agda

Bend/Fun/FanKind/

0/

  • FanKind.agda

Bend/Fun/FnDef/

0/

  • FnDef.agda
  • new-gen.agda
  • show.agda

Bend/Fun/MatchRule/

0/

  • MatchRule.agda
  • show.agda

Bend/Fun/Num/

0/

  • Num.agda
  • show.agda

Bend/Fun/Op/

0/

  • Op.agda
  • show.agda

Bend/Fun/Pattern/

0/

  • Pattern.agda
  • binds.agda
  • children.agda
  • map-binds.agda
  • map-children.agda
  • show.agda
  • unscoped-binds.agda

Bend/Fun/Rule/

0/

  • Rule.agda

Bend/Fun/Term/

0/

  • Term.agda
  • children-with-binds.agda
  • children.agda
  • free-vars.agda
  • is-ref.agda
  • map-child-binds.agda
  • map-children-with-binds.agda
  • map-children-with-state.agda
  • show.agda
  • unscoped-vars.agda

Bend/Fun/Type/

0/

  • Type.agda
  • show.agda

Bend/Fun/

0/

  • dsl.agda
  • show-bind.agda

Bend/Load/

0/

  • load-book.agda

Bend/Net/

0/

  • Net.agda
  • get-node.agda
  • get-port.agda
  • link.agda
  • net-root.agda
  • new-node.agda
  • new.agda
  • set-port.agda
  • show.agda

Bend/Net/Node/

0/

  • Node.agda
  • get.agda
  • set.agda
  • show.agda

Bend/Net/NodeKind/

0/

  • NodeKind.agda
  • from-fan-kind.agda
  • show.agda

Bend/Net/Port/

0/

  • Port.agda
  • show.agda
  • to-bits.agda
  • to-pair.agda

Bend/Parser/Fun/

0/

  • parse-adt.agda
  • parse-book.agda
  • parse-def-sig.agda
  • parse-fn-def.agda
  • parse-pattern.agda
  • parse-rule-lhs.agda
  • parse-term.agda
  • parse-type-term.agda

Bend/Parser/ParseBook/

0/

  • ParseBook.agda
  • TopLevel.agda
  • new.agda

Bend/Parser/

0/

  • consume-exactly.agda
  • consume.agda
  • first-with-guard.agda
  • is-digit-radix.agda
  • is-name-char.agda
  • list-like.agda
  • parse-keyword.agda
  • parse-number.agda
  • parse-oper.agda
  • parse-restricted-name.agda
  • parse-top-level-name.agda
  • parse-var-name.agda
  • sep-by.agda
  • skip-trivia.agda
  • starts-with-keyword.agda
  • try-consume-exactly.agda
  • try-consume.agda

Bend/Run/

0/

  • show-hvm.agda
  • to-bend-core.agda
  • to-hvm.agda

Bend/Source/

0/

  • Source.agda
  • SourceKind.agda
  • TextLocation.agda
  • TextSpan.agda
  • from-file-span.agda
  • is-builtin.agda

Bend/Transform/FloatCombinators/

0/

  • Ctx.agda
  • float-combinators.agda
  • is-safe.agda
  • map-float-children.agda

Bend/Transform/

0/

  • encode-adts.agda
  • linearize-vars.agda
  • resolve-refs.agda
  • subst.agda
  • unbound-refs.agda
  • unbound-vars.agda
  • unique-names.agda

Bend/

0/

  • nat-to-name.agda

Debug/

0/

  • Trace.agda

HVM/Addr/

0/

  • Addr.agda

HVM/Mode/

0/

  • Mode.agda
  • is-wired.agda

HVM/Net/

0/

  • Net.agda
  • show.agda

HVM/Parser/

0/

  • parse-net.agda
  • parse-redex.agda
  • parse-term.agda

HVM/Redex/

0/

  • Redex.agda
  • show.agda

HVM/Rule/

0/

  • anni.agda
  • comm.agda
  • eras.agda
  • link.agda
  • void.agda

HVM/Run/Monad/

0/

  • bind.agda
  • pure.agda

HVM/Run/

0/

  • Run.agda
  • enter.agda
  • evaluate.agda
  • fresh.agda
  • interact.agda
  • link.agda
  • materialize.agda
  • normalize.agda
  • redex-pop.agda
  • redex-push.agda
  • state-get.agda
  • state-mut.agda
  • subst-swap.agda
  • subst-take.agda

HVM/Run/State/

0/

  • State.agda
  • boot.agda

HVM/Term/

0/

  • Term.agda
  • show.agda

Imp/Backend/Cuda/

0/

  • grid-to-cuda.agda

Imp/Eval/Config/Grid/

0/

  • Grid.agda

Imp/Eval/Env/

0/

  • Env.agda
  • get.agda
  • pop.agda
  • push.agda
  • set.agda

Imp/Eval/Frame/

0/

  • Frame.agda

Imp/Eval/Memory/

0/

  • Memory.agda

Imp/Eval/State/Block/

0/

  • Block.agda
  • step.agda

Imp/Eval/State/Grid/

0/

  • Grid.agda
  • step.agda

Imp/Eval/State/Thread/

0/

  • Thread.agda
  • step.agda

Imp/Eval/

0/

  • eval-expr.agda

Imp/Expr/

0/

  • Expr.agda
  • show.agda

Imp/

0/

  • Notation.agda

Imp/Stmt/

0/

  • Stmt.agda
  • show.agda

UG/Chat/Client/

0/

  • Client.agda
  • handle-pong.agda
  • join-room.agda
  • send.agda
  • sync-time.agda

UG/Chat/Message/

0/

  • Message.agda
  • to-nat.agda

UG/SIPD/Event/Click/

0/

  • Click.agda
  • deserialize.agda
  • serialize.agda
  • show.agda

UG/SIPD/Event/

0/

  • Event.agda
  • deserialize.agda
  • get-events.agda
  • serialize.agda
  • show.agda

UG/SIPD/Player/

0/

  • Player.agda
  • draw.agda
  • init.agda

UG/SIPD/Renderer/

0/

  • Renderer.agda
  • clear.agda
  • create.agda
  • present.agda
  • set-renderer-draw-color.agda

UG/SIPD/State/

0/

  • State.agda
  • draw.agda
  • init.agda

UG/SIPD/Video/

0/

  • init.agda
  • quit.agda

UG/SIPD/Window/

0/

  • Window.agda
  • create.agda

UG/SIPD/

0/

  • draw.agda

UG/SM/ActionLogs/

0/

  • ActionLogs.agda
  • add-action.agda
  • get-actions.agda

UG/SM/Game/

0/

  • Game.agda

UG/SM/

0/

  • SM.agda
  • action-in-list.agda
  • add-action-to-logs.agda
  • compute.agda
  • get-initial-state.agda
  • new-mach.agda
  • register-action.agda
  • remove-future-states.agda
  • update-cached-tick.agda
  • update-genesis-tick.agda
  • update-mach.agda

UG/SM/StateLogs/

0/

  • StateLogs.agda
  • find-rollback-amount.agda
  • push.agda
  • rollback.agda

UG/SM/Tick/

0/

  • Tick.agda

UG/SM/Time/

0/

  • Time.agda
  • time-to-tick.agda

UG/SM/TimedAction/

0/

  • TimedAction.agda

UG/Shape/

0/

  • Shape.agda
  • draw.agda
  • square.agda

./ARC/DSL/Functions/

1/

  • branch.agda
  • chain.agda
  • fork.agda
  • rbind.agda

11/

  • argmax.agda

12/

  • remove.agda

13/

  • leastcommon.agda
  • mostcommon.agda

14/

  • leastcolor.agda
  • mostcolor.agda

2/

  • both.agda
  • dedupe.agda
  • difference.agda
  • either.agda
  • equality.agda
  • flip.agda
  • pair.agda

3/

  • aslist.agda
  • even.agda
  • greater.agda
  • insert.agda
  • int-cmp.agda
  • intersection.agda
  • lbind.agda
  • matcher.agda
  • positive.agda
  • toivec.agda
  • tojvec.agda

4/

  • mpapply.agda
  • power.agda
  • rapply.agda
  • repeat.agda
  • tolist.agda

5/

  • add.agda
  • apply.agda
  • argmin.agda
  • decrement.agda
  • divide.agda
  • double.agda
  • extract.agda
  • first.agda
  • halve.agda
  • increment.agda
  • initset.agda
  • interval.agda
  • invert.agda
  • mapply.agda
  • maximum.agda
  • multiply.agda
  • other.agda
  • product.agda
  • subtract.agda

6/

  • combine.agda
  • container-to-list.agda
  • last.agda
  • mfilter.agda
  • papply.agda
  • size.agda

7/

  • crement.agda
  • merge.agda
  • sfilter.agda

8/

  • prapply.agda
  • sign.agda

9/

  • contained.agda
  • height.agda
  • order.agda
  • valmax.agda
  • valmin.agda

./ARC/DSL/Types/Boolean/

1/

  • Boolean.agda
  • Functions.agda

./ARC/DSL/Types/Integer/

1/

  • Functions.agda
  • Integer.agda

./ARC/DSL/Types/List/

1/

  • Functions.agda
  • List.agda

./ARC/DSL/Types/ListList/

1/

  • ListList.agda

./ARC/DSL/Types/OrdSet/

1/

  • Functions.agda
  • OrdSet.agda

./ARC/DSL/Types/Pair/

1/

  • Functions.agda
  • Pair.agda

./ARC/DSL/Types/Union/

1/

  • Functions.agda
  • Union.agda

./Base/BinTree/

1/

  • fold.agda

11/

  • ALL.agda

2/

  • merge.agda

3/

  • sum.agda

4/

  • eq.agda
  • show.agda

5/

  • all-equal.agda
  • neq.agda

6/

  • count.agda

7/

  • eq-.agda
  • show-.agda

./Base/Bits/

1/

  • and.agda
  • append.agda
  • dec.agda
  • inc.agda
  • normal.agda
  • not.agda
  • or.agda
  • pred.agda
  • reverse.agda
  • succ.agda
  • xor.agda

14/

  • encode-char-utf8.agda

2/

  • add.agda
  • concat.agda
  • eq.agda
  • gt.agda
  • length.agda
  • lshift.agda
  • lt.agda
  • mul.agda
  • pad-zeros.agda
  • rshift.agda
  • take.agda

3/

  • add-.agda
  • dec-.agda
  • is-zero.agda
  • normal-.agda
  • not-.agda
  • or-.agda
  • reverse-.agda
  • show.agda
  • xor-.agda

4/

  • concat-.agda
  • div-.agda
  • eq-.agda
  • from-nat-.agda
  • gt-.agda
  • gte.agda
  • inc-.agda
  • length-.agda
  • lte.agda
  • mod-.agda
  • neq.agda
  • pad-zeros-.agda
  • pred-.agda
  • show-.agda
  • show-rev.agda
  • split-at.agda
  • succ-.agda
  • to-nat-.agda
  • to-nat.agda

47/

  • ALL.agda

5/

  • compare.agda
  • div.agda
  • from-char.agda
  • lshift-.agda
  • lt-.agda
  • mod.agda
  • rshift-.agda
  • split-chunks.agda
  • sub-.agda
  • sub.agda
  • to-char.agda

6/

  • and-.agda
  • append-.agda
  • decode-utf8.agda
  • mul-.agda

7/

  • conversion-tests-.agda
  • pad-length.agda

8/

  • from-nat.agda

9/

  • encode-utf8.agda
  • pad-length-.agda

./Base/Bool/

1/

  • and.agda
  • eq.agda
  • if.agda
  • neq.agda
  • not.agda
  • or.agda
  • xor.agda

11/

  • ALL.agda

2/

  • show.agda

3/

  • eq-.agda
  • neq-.agda
  • not-.agda
  • or-.agda

4/

  • show-.agda

./Base/ByteString/

1/

  • append.agda
  • tail.agda

11/

  • pack-string-fixed.agda

14/

  • read-u48.agda

18/

  • write-u48.agda

2/

  • concat.agda
  • cons.agda
  • head.agda
  • is-empty.agda
  • show.agda
  • take.agda

21/

  • ALL.agda

3/

  • pack-string.agda
  • unpack.agda

4/

  • pack.agda

5/

  • drop.agda
  • read-f64.agda

7/

  • slice.agda

8/

  • write-f64-as-nat.agda

9/

  • read-char.agda

./Base/Char/

1/

  • Char.agda
  • to-lower.agda
  • to-upper.agda

11/

  • to-digit.agda

2/

  • eq.agda
  • from-nat.agda
  • is-alpha.agda
  • is-ascii.agda
  • is-digit.agda
  • is-hex-digit.agda
  • is-latin1.agda
  • is-lower.agda
  • is-print.agda
  • is-space.agda
  • to-nat.agda

27/

  • ALL.agda

3/

  • digit-to-nat.agda

4/

  • compare.agda
  • eq-.agda
  • gt.agda
  • gte.agda
  • hex-to-nat.agda
  • lt.agda
  • lte.agda
  • neq.agda
  • show-.agda
  • show.agda

./Base/DiffList/

1/

  • DiffList.agda

2/

  • cons.agda
  • empty.agda
  • snoc.agda
  • to-list.agda

3/

  • append.agda

6/

  • ALL.agda

./Base/Either/

1/

  • ALL.agda

./Base/Empty/

1/

  • ALL.agda

./Base/Equal/

1/

  • apply.agda
  • erase.agda
  • subst.agda
  • sym.agda
  • trans.agda

3/

  • left.agda
  • right.agda

8/

  • ALL.agda

./Base/F64/

1/

  • acos.agda
  • add.agda
  • asin.agda
  • atan.agda
  • cos.agda
  • cosh.agda
  • div.agda
  • exp.agda
  • log.agda
  • mul.agda
  • negate.agda
  • sin.agda
  • sinh.agda
  • sqrt.agda
  • sub.agda
  • tan.agda
  • tanh.agda

2/

  • double.agda
  • eq.agda
  • from-int.agda
  • from-nat.agda
  • half.agda
  • lt.agda
  • show.agda
  • square.agda

24/

  • from-string.agda

3/

  • floor.agda
  • gt.agda
  • max.agda
  • min.agda
  • sub-.agda
  • to-u64.agda

4/

  • from-u64.agda
  • gte.agda
  • lte.agda
  • mod.agda
  • neq-.agda
  • neq.agda

45/

  • ALL.agda

5/

  • and.agda
  • compare.agda
  • or.agda
  • show-.agda

6/

  • from-bits.agda
  • to-bits.agda

8/

  • eq-.agda

9/

  • add-.agda

./Base/IO/Monad/

1/

  • bind.agda
  • pure.agda

./Base/List/Monad/

1/

  • pure.agda

2/

  • bind.agda

./Base/List/Omega/

1/

  • Omega.agda

2/

  • each.agda

3/

  • take.agda

./Base/List/

1/

  • append.agda
  • foldl.agda
  • foldr.agda
  • intersperse.agda
  • map.agda
  • match.agda
  • singleton.agda
  • zip-with.agda

10/

  • sort-.agda

11/

  • frequency.agda

2/

  • drop-while.agda
  • drop.agda
  • empty.agda
  • filter.agda
  • head.agda
  • insert-at-sorted.agda
  • insert-at.agda
  • intercalate.agda
  • is-cons.agda
  • is-nil.agda
  • iterate.agda
  • last.agda
  • length.agda
  • mfoldl.agda
  • mmap.agda
  • replicate.agda
  • reverse.agda
  • tail.agda
  • tails.agda
  • take-while.agda
  • take.agda
  • unzip-with.agda
  • update-at.agda
  • zip-cons.agda

3/

  • cartesian-product.agda
  • compare.agda
  • concat-map.agda
  • concat-maybes.agda
  • concat.agda
  • find.agda
  • gt.agda
  • gte.agda
  • inits.agda
  • insertion-sort.agda
  • lookup.agda
  • lt.agda
  • lte.agda
  • sort.agda
  • split-chunks.agda
  • unsnoc.agda
  • unzip.agda
  • zip.agda

4/

  • all-equal.agda
  • all-true.agda
  • and.agda
  • any-true.agda
  • cartesian-product-with.agda
  • contains.agda
  • diagonal.agda
  • eq.agda
  • or.agda
  • product.agda
  • show.agda
  • split-first.agda
  • sum.agda

5/

  • difference.agda
  • neq-.agda
  • neq.agda
  • remove-at.agda
  • split-at-element.agda
  • split-at.agda

6/

  • count.agda
  • eq-.agda
  • quicksort.agda
  • show-.agda

7/

  • dedup.agda
  • is-asc.agda

8/

  • split-last.agda
  • starts-with.agda

84/

  • ALL.agda

./Base/Maybe/Monad/

1/

  • bind.agda
  • pure.agda

./Base/Maybe/

1/

  • fold.agda
  • map.agda
  • run.agda

15/

  • ALL.agda

2/

  • to-bool.agda
  • to-list.agda
  • to-result.agda

3/

  • eq.agda

4/

  • show.agda

5/

  • neq.agda

./Base/Nat/

1/

  • add.agda
  • double.agda
  • half.agda
  • match.agda
  • pred.agda
  • sub.agda

2/

  • compare.agda
  • eq.agda
  • exp.agda
  • is-zero.agda
  • lt.agda
  • mod.agda
  • mul.agda
  • show.agda
  • to-u64.agda

3/

  • div.agda
  • gt.agda
  • gte.agda
  • half-.agda
  • max-.agda
  • min-.agda
  • pred-.agda
  • rshift-.agda
  • rshift.agda
  • xor-.agda

31/

  • ALL.agda

4/

  • add-.agda
  • compare-.agda
  • double-.agda
  • exp-.agda
  • gt-.agda
  • gte-.agda
  • is-zero-.agda
  • lt-.agda
  • lte-.agda
  • match-.agda
  • max.agda
  • min.agda
  • neq-.agda
  • neq.agda
  • range.agda
  • show-.agda
  • to-bits-.agda
  • xor.agda

5/

  • eq-.agda
  • lte.agda
  • mod-.agda
  • mul-.agda
  • sub-.agda

6/

  • range-.agda
  • to-bits.agda

7/

  • div-.agda
  • to-u64-.agda

./Base/Pair/

1/

  • get-fst.agda
  • get-snd.agda
  • map.agda
  • mut-fst.agda
  • mut-snd.agda
  • set-fst.agda
  • set-snd.agda

14/

  • ALL.agda

2/

  • to-list.agda

4/

  • eq.agda
  • show.agda

5/

  • neq.agda

7/

  • neq-.agda

8/

  • show-.agda

9/

  • eq-.agda

./Base/Parser/Examples/LambdaTerm/

1/

  • LambdaTerm.agda

12/

  • parse.agda

2/

  • new.agda

./Base/Parser/

1/

  • Reply.agda

10/

  • bind-.agda
  • parse-char-.agda

11/

  • parse-string.agda

12/

  • parse-quoted-char-.agda

13/

  • advance-one.agda

14/

  • advance-many.agda

15/

  • peek-many.agda
  • take-while.agda

16/

  • parse-name.agda
  • skip-spaces.agda

19/

  • consume.agda

2/

  • Error.agda
  • State.agda

20/

  • parse-char.agda

21/

  • skip-trivia.agda

25/

  • ALL.agda

4/

  • Parser.agda
  • map.agda

5/

  • Error-.agda
  • State-.agda
  • alternative.agda
  • fail.agda

6/

  • Reply-.agda
  • get-index.agda
  • parse-quoted-char.agda

7/

  • fail-.agda
  • is-eof.agda
  • starts-with.agda

8/

  • Test-.agda
  • is-eof-.agda
  • parse-name-.agda
  • parse-string-.agda
  • peek-one.agda
  • pure-.agda
  • skip-spaces-.agda
  • skip-trivia-.agda
  • starts-with-.agda

9/

  • advance-many-.agda
  • advance-one-.agda
  • consume-.agda
  • parse-many.agda
  • peek-many-.agda
  • peek-one-.agda
  • take-while-.agda

./Base/Result/Monad/

1/

  • bind.agda

./Base/Result/

1/

  • fold.agda

4/

  • ALL.agda

./Base/String/

1/

  • String.agda
  • append.agda
  • show.agda

10/

  • to-nat-base.agda

16/

  • hash.agda

2/

  • eq.agda

3/

  • from-list.agda
  • show-.agda
  • to-list.agda

30/

  • ALL.agda

4/

  • contains-.agda
  • contains.agda
  • eq-.agda
  • from-char.agda
  • length.agda
  • lte-.agda
  • neq-.agda
  • neq.agda
  • uncons.agda

5/

  • foldr.agda
  • head.agda
  • is-empty.agda
  • replicate.agda
  • to-nat-base-.agda

6/

  • compare.agda
  • drop.agda
  • gt.agda
  • gte.agda
  • join.agda
  • lt.agda
  • lte.agda
  • split-at.agda

7/

  • starts-with.agda

8/

  • join-.agda

./Base/Time/

1/

  • ALL.agda

2/

  • now.agda

./Base/Trait/

1/

  • Monoid.agda
  • Show.agda

2/

  • Eq.agda

4/

  • Ord.agda

6/

  • ALL.agda

./Base/V2/

1/

  • V2.agda

2/

  • div.agda
  • sub.agda

21/

  • ALL.agda

3/

  • add.agda
  • div-scalar.agda
  • max.agda
  • min.agda
  • mul-scalar.agda
  • negate.agda
  • normalize.agda
  • perpendicular.agda

4/

  • dist.agda
  • dot.agda
  • show.agda

5/

  • eq.agda
  • length.agda
  • lerp.agda
  • sqr-dist.agda

6/

  • neq.agda

./Bend/Net/Port/

1/

  • Port.agda

3/

  • to-pair.agda

5/

  • to-bits.agda

7/

  • show.agda

./Bend/Net/

1/

  • net-root.agda

14/

  • show-.agda
  • show.agda

4/

  • Net.agda

5/

  • link.agda

8/

  • get-node.agda
  • get-port.agda
  • new-node.agda
  • new.agda
  • set-port.agda

./Bend/Source/

1/

  • TextLocation.agda
  • TextSpan.agda

3/

  • is-builtin.agda

4/

  • Source.agda
  • from-file-span.agda

./Imp/Eval/Memory/

1/

  • Memory.agda

./

1/

  • Main.agda

10/

  • T0-.agda

7/

  • T1-.agda

./UG/Chat/Message/

1/

  • Message.agda

2/

  • to-nat.agda

./UG/SM/Tick/

1/

  • Tick.agda

./UG/SM/Time/

1/

  • Time.agda

6/

  • time-to-tick.agda

./UG/SM/TimedAction/

1/

  • TimedAction.agda

./ARC/DSL/Types/Grid/

2/

  • Grid.agda

./ARC/DSL/Types/Indices/

2/

  • Indices.agda

./ARC/DSL/Types/IndicesSet/

2/

  • IndicesSet.agda

./ARC/DSL/Types/IntegerList/

2/

  • IntegerList.agda

./ARC/DSL/Types/IntegerSet/

2/

  • IntegerSet.agda

./ARC/DSL/Types/Numerical/

2/

  • Numerical.agda

./ARC/DSL/Types/Object/

2/

  • Object.agda

./ARC/DSL/Types/Objects/

2/

  • Objects.agda

./Base/AVLTree/

10/

  • has-key-.agda
  • rotate-left-.agda
  • rotate-right-.agda

11/

  • insert.agda

12/

  • intersect.agda

15/

  • insert-.agda

18/

  • fold-.agda
  • intersect-.agda
  • union-.agda

19/

  • delete-.agda

2/

  • AVLTree.agda
  • empty.agda
  • fold.agda

20/

  • difference-.agda

3/

  • height.agda
  • maximum.agda
  • minimum.agda
  • singleton.agda
  • size.agda

33/

  • ALL.agda

4/

  • delete.agda
  • to-list.agda

5/

  • get-pair.agda
  • get.agda
  • has-key.agda
  • keys.agda
  • union.agda
  • values.agda

6/

  • invert.agda
  • map-keys.agda
  • map-values.agda
  • map.agda

7/

  • from-list.agda

8/

  • difference.agda

9/

  • filter.agda
  • is-balanced.agda

./Base/AVLTree/Balance/

2/

  • eq.agda
  • neq.agda

6/

  • rotate-left.agda
  • rotate-right.agda

./Base/BitMap/

2/

  • BitMap.agda
  • empty.agda
  • new.agda

20/

  • ALL.agda

3/

  • merge.agda

4/

  • count.agda
  • del.agda
  • get.agda
  • values.agda

5/

  • contains.agda
  • show.agda
  • swap.agda
  • take.agda

6/

  • insert.agda
  • set.agda
  • union.agda

7/

  • difference.agda
  • from-list.agda
  • to-list.agda

./Base/Concurrent/Channel/

2/

  • new.agda

3/

  • read.agda
  • write.agda

./Base/IO/

15/

  • ALL.agda

2/

  • get-line.agda
  • read-file.agda

3/

  • append-file.agda
  • delete-file.agda
  • is-directory.agda
  • is-file.agda
  • mkdir.agda
  • print.agda
  • write-file.agda

4/

  • get-args.agda

8/

  • exists.agda

./Base/Int/

18/

  • ALL.agda

2/

  • Int.agda
  • from-nat.agda
  • from-neg.agda

3/

  • neg.agda
  • to-nat.agda

4/

  • compare.agda
  • eq.agda
  • gt.agda
  • gte.agda
  • lt.agda
  • lte.agda
  • mul.agda
  • neq.agda

5/

  • show.agda
  • to-bits.agda

./Base/List/Omega/Monad/

2/

  • pure.agda

4/

  • bind.agda

./Base/Nat/div/

2/

  • go.agda

./Base/Network/HTTP/Method/

2/

  • to-string.agda

./Base/Network/HTTP/

2/

  • fetch.agda

./Base/OrdMap/

16/

  • ALL.agda

2/

  • OrdMap.agda
  • empty.agda
  • fold.agda

3/

  • difference.agda
  • intersect.agda
  • keys.agda
  • values.agda

4/

  • singleton.agda

5/

  • delete.agda
  • get-pair.agda
  • get.agda
  • insert.agda
  • to-list.agda
  • union.agda

6/

  • from-list.agda
  • has-key.agda

./Base/OrdSet/

17/

  • ALL.agda

2/

  • OrdSet.agda
  • empty.agda

3/

  • delete.agda
  • difference.agda
  • intersect.agda
  • map.agda
  • size.agda
  • union.agda

4/

  • contains.agda
  • fold.agda
  • maximum.agda
  • minimum.agda
  • to-list.agda

5/

  • insert.agda
  • singleton.agda

7/

  • from-list.agda

9/

  • filter.agda

./Base/Ordering/

2/

  • eq.agda
  • neq.agda

4/

  • ALL.agda

./Base/Queue/

2/

  • enqueue.agda

3/

  • ALL.agda

4/

  • Queue.agda

5/

  • dequeue.agda

./Base/U64/

10/

  • div.agda

2/

  • U64.agda
  • double.agda
  • to-nat.agda

3/

  • from-bool.agda
  • from-nat.agda

30/

  • ALL.agda

4/

  • add.agda
  • gt.agda
  • gte.agda
  • if.agda
  • lt.agda
  • lte.agda
  • mod.agda
  • mul.agda
  • neq.agda

5/

  • compare.agda
  • eq.agda
  • max.agda
  • min.agda
  • show.agda
  • sub.agda
  • to-bits.agda

6/

  • from-bits.agda

7/

  • and.agda
  • not.agda
  • or.agda
  • xor.agda

./Base/Unit/

2/

  • eq.agda
  • neq.agda

4/

  • ALL.agda

./Base/Word8/

2/

  • from-nat.agda
  • to-nat.agda

3/

  • ALL.agda

./Bend/Fun/Pattern/

12/

  • show.agda

2/

  • children.agda

3/

  • map-children.agda

4/

  • map-binds.agda

5/

  • Pattern.agda
  • unscoped-binds.agda

6/

  • binds.agda

./Bend/Fun/Rule/

2/

  • Rule.agda

./Bend/Fun/Term/

10/

  • Term.agda

11/

  • unscoped-vars.agda

12/

  • free-vars-.agda
  • unscoped-vars-.agda

14/

  • children-with-binds.agda

15/

  • map-child-binds.agda
  • map-children-with-binds.agda

18/

  • free-vars.agda

2/

  • is-ref.agda

21/

  • show.agda

22/

  • show-.agda

6/

  • map-children.agda

7/

  • map-children-with-state.agda

8/

  • children.agda

./Bend/Fun/Type/

11/

  • show.agda

2/

  • Type.agda

3/

  • from-fn-sig.agda

./Bend/Net/Node/

10/

  • show.agda

2/

  • Node.agda

5/

  • get.agda
  • set.agda

./Bend/Net/NodeKind/

2/

  • NodeKind.agda
  • from-fan-kind.agda

7/

  • show.agda

./Bend/Parser/ParseBook/

2/

  • new.agda

5/

  • ParseBook.agda

6/

  • TopLevel.agda

./Debug/

2/

  • Trace.agda

./HVM/Mode/

2/

  • is-wired.agda

./HVM/Redex/

2/

  • Redex.agda

5/

  • show.agda

./UG/SIPD/Event/Click/

2/

  • show.agda

6/

  • deserialize.agda
  • serialize.agda

./UG/SIPD/Video/

2/

  • init.agda
  • quit.agda

./UG/SIPD/Window/

2/

  • create.agda

./ARC/DSL/Types/Cell/

3/

  • Cell.agda

./ARC/DSL/Types/Element/

3/

  • Element.agda

./ARC/DSL/Types/Patch/

3/

  • Patch.agda

./ARC/DSL/Types/Piece/

3/

  • Piece.agda

./Base/BinTree/Trait/

3/

  • Show.agda

4/

  • Eq.agda

./Base/BitMap/Trait/

3/

  • Show.agda

./Base/Bits/Trait/

3/

  • Show.agda

4/

  • Eq.agda

7/

  • Ord.agda

./Base/Bool/Trait/

3/

  • Show.agda

4/

  • Eq.agda

./Base/Buffer/

11/

  • set.agda

3/

  • Buffer.agda

4/

  • ALL.agda

7/

  • get.agda

9/

  • new.agda

./Base/ByteString/Trait/

3/

  • Show.agda

./Base/Char/Trait/

3/

  • Show.agda

4/

  • Eq.agda

7/

  • Ord.agda

./Base/F64/Trait/

3/

  • Show.agda

4/

  • Eq.agda

7/

  • Ord.agda

./Base/Function/

3/

  • ALL.agda

./Base/Int/Trait/

3/

  • Show.agda

4/

  • Eq.agda

7/

  • Ord.agda

./Base/JSON/Trait/

3/

  • Show.agda

./Base/List/Trait/

3/

  • Show.agda

4/

  • Eq.agda
  • Monad.agda

7/

  • Ord.agda

./Base/Maybe/Trait/

3/

  • Show.agda

4/

  • Eq.agda
  • Monad.agda

./Base/Nat/Trait/

3/

  • Add.agda
  • Show.agda

4/

  • Eq.agda

7/

  • Ord.agda

./Base/Network/WebSocket/

3/

  • receive-data.agda

4/

  • send-close.agda
  • send-text-data.agda

5/

  • receive-binary-data.agda
  • run-client.agda
  • run-concurrent-client.agda
  • run-secure-client.agda
  • send-binary-data.agda

./Base/Pair/Trait/

3/

  • Show.agda

4/

  • Eq.agda

./Base/Result/Trait/

3/

  • Monad.agda

./Base/String/Trait/

3/

  • Monoid.agda
  • Show.agda

4/

  • Eq.agda

7/

  • Ord.agda

./Base/U64/Trait/

3/

  • Show.agda

4/

  • Eq.agda

7/

  • Ord.agda

./Base/V2/Trait/

3/

  • Show.agda

4/

  • Eq.agda

./Bend/Cli/Command/

3/

  • from-string.agda

./Bend/Compile/NetToHvm/State/

3/

  • State.agda

4/

  • new.agda

./Bend/Fun/Adt/

3/

  • Adt.agda
  • CtrField.agda

5/

  • Ctr.agda

./Bend/Fun/MatchRule/

14/

  • show.agda

3/

  • MatchRule.agda

./Bend/Fun/Num/

3/

  • Num.agda

8/

  • show.agda

./Bend/Fun/Op/

3/

  • show.agda

./Bend/Fun/

27/

  • dsl.agda

3/

  • show-bind.agda

./Bend/Parser/

10/

  • parse-number-.agda

12/

  • sep-by.agda

14/

  • starts-with-keyword-.agda

16/

  • list-like.agda

17/

  • skip-trivia-.agda

20/

  • list-like-.agda
  • parse-restricted-name.agda
  • sep-by-.agda

22/

  • skip-trivia.agda

23/

  • starts-with-keyword.agda

3/

  • parse-top-level-name.agda
  • parse-var-name.agda

4/

  • consume-exactly.agda

49/

  • parse-number.agda

5/

  • is-name-char-.agda

6/

  • consume.agda
  • first-with-guard.agda
  • is-name-char.agda

7/

  • is-digit-radix.agda
  • try-consume-exactly.agda

8/

  • parse-oper.agda
  • try-consume.agda

9/

  • parse-keyword.agda
  • try-parse-keyword.agda

./HVM/Addr/

3/

  • Addr.agda

./HVM/Run/

11/

  • subst-take.agda

12/

  • evaluate.agda
  • subst-swap.agda

13/

  • link.agda

16/

  • interact.agda

3/

  • Run.agda

4/

  • get.agda
  • state-get.agda

5/

  • state-mut.agda
  • state-set.agda

7/

  • boot.agda

8/

  • enter.agda
  • materialize.agda
  • normalize.agda

9/

  • fresh.agda
  • redex-pop.agda
  • redex-push.agda

./Imp/Eval/Config/Grid/

3/

  • Grid.agda

./Imp/Eval/Env/

3/

  • pop.agda
  • push.agda

4/

  • Env.agda

7/

  • get.agda

8/

  • set.agda

./Imp/Eval/Frame/

3/

  • Frame.agda

./Imp/Eval/State/Grid/

11/

  • step.agda

3/

  • Grid.agda

8/

  • run.agda

./UG/SIPD/Renderer/

3/

  • clear.agda
  • create.agda
  • present.agda

4/

  • set-renderer-draw-color.agda

./UG/Shape/

3/

  • Shape.agda
  • circle.agda

4/

  • triangle.agda

6/

  • draw.agda
  • square.agda

7/

  • pentagon.agda

./Base/AVLTree/Balance/Trait/

4/

  • Eq.agda

./Base/BitMap/Test/

10/

  • merge.agda
  • show.agda
  • to-list.agda

12/

  • take.agda

14/

  • from-list.agda

4/

  • empty.agda
  • new.agda

7/

  • count.agda

8/

  • contains.agda
  • get.agda
  • set.agda

9/

  • del.agda
  • swap.agda

./Base/Concurrent/

4/

  • ALL.agda

./Base/IO/Trait/

4/

  • Monad.agda

./Base/Int/Test/

4/

  • from-neg.agda

./Base/List/Tm/

4/

  • is-cons.agda
  • is-nil.agda

./Base/Ordering/Trait/

4/

  • Eq.agda

./Base/Parser/Monad/

4/

  • pure.agda

5/

  • bind.agda

./Base/U64/Test/

4/

  • eq.agda
  • show.agda

./Base/Unit/Trait/

4/

  • Eq.agda

./Bend/Fun/Book/

17/

  • show.agda

4/

  • new.agda

5/

  • Book.agda
  • add-fn-def.agda
  • contains-def.agda

6/

  • get-adt.agda
  • get-ctr.agda

./Bend/Run/

12/

  • to-bend-core.agda

4/

  • show-hvm.agda

6/

  • to-hvm.agda

./HVM/Net/

10/

  • show.agda

4/

  • Net.agda

./HVM/Rule/

10/

  • link.agda

4/

  • void.agda

7/

  • anni.agda
  • eras.agda

8/

  • comm.agda

./HVM/Run/Monad/

4/

  • bind.agda
  • pure.agda

./HVM/Term/

4/

  • show.agda

5/

  • Term.agda

./Imp/Eval/State/Block/

13/

  • step.agda

4/

  • Block.agda

./UG/Chat/Client/

14/

  • exit-room.agda
  • join-room.agda
  • send.agda
  • sync-time.agda

16/

  • handle-pong.agda

19/

  • handle-message.agda

4/

  • Client.agda

5/

  • time.agda

./UG/SIPD/Event/

15/

  • Main.agda

17/

  • deserialize.agda

20/

  • serialize.agda

4/

  • Event.agda

6/

  • get-events.agda

7/

  • show.agda

./UG/SIPD/Player/

20/

  • draw.agda

4/

  • Player.agda

9/

  • init.agda

./UG/SM/StateLogs/

4/

  • push.agda

5/

  • StateLogs.agda

8/

  • rollback.agda

9/

  • find-rollback-amount.agda

./UG/SM/

26/

  • register-action.agda

30/

  • compute.agda

4/

  • action-in-list.agda
  • add-action-to-logs.agda

5/

  • SM.agda
  • update-cached-tick.agda
  • update-mach.agda

6/

  • update-genesis-tick.agda

7/

  • remove-future-states.agda

8/

  • new-mach.agda

9/

  • get-initial-state.agda

./ARC/DSL/Types/Container/

5/

  • Functions.agda

6/

  • Container.agda

./Base/JSON/

10/

  • ALL.agda

11/

  • parse-object.agda

14/

  • show.agda

15/

  • parse.agda

21/

  • parse-number.agda

25/

  • parse-string.agda

5/

  • JSON.agda

6/

  • parse-null.agda

8/

  • parse-array.agda
  • parse-bool.agda

./Bend/Compile/BendToNet/Encoder/

11/

  • link-var.agda

15/

  • encode-pat.agda

21/

  • encode-term.agda

5/

  • encode-num.agda
  • link.agda
  • new-node.agda
  • new.agda

7/

  • Encoder.agda

./Imp/Expr/

5/

  • Expr.agda
  • show.agda

./Imp/

11/

  • Main-Cuda.agda

5/

  • Notation.agda

./UG/SIPD/State/

13/

  • draw.agda

5/

  • State.agda

9/

  • init.agda

./Base/BitMap/Tm/

6/

  • get-set.agda

./Base/List/Test/

10/

  • split-last.agda

6/

  • unsnoc.agda

8/

  • split-chunks.agda

./Base/Maybe/Test/

6/

  • eq.agda
  • show.agda

./Bend/Fun/FnDef/

11/

  • new-gen.agda

13/

  • show.agda

6/

  • FnDef.agda

./Bend/Transform/FloatCombinators/

21/

  • is-safe.agda

45/

  • float-combinators.agda

6/

  • map-float-children.agda

9/

  • Ctx.agda

./Bend/

12/

  • nat-to-name.agda

24/

  • bend.agda

6/

  • nat-to-name-.agda

./Imp/Eval/State/Thread/

23/

  • step.agda

6/

  • Thread.agda

./Imp/Stmt/

6/

  • Stmt.agda

7/

  • show.agda

9/

  • show-.agda

./UG/SM/ActionLogs/

6/

  • get-actions.agda

8/

  • ActionLogs.agda

9/

  • add-action.agda

./Base/BitMap/Examples/

7/

  • mutation.agda

./Base/Bits/Decode-utf8/

7/

  • decode-utf8-go.agda

./Bend/Compile/NetToHvm/

15/

  • net-to-hvm.agda

17/

  • get-redexes.agda

23/

  • tree-to-hvm.agda

7/

  • nets-to-hvm.agda

./Bend/Transform/

16/

  • unbound-refs.agda

24/

  • resolve-refs.agda

26/

  • linearize-vars-.agda

27/

  • unique-names-.agda

28/

  • unique-names.agda

32/

  • resolve-refs-.agda

35/

  • linearize-vars.agda

42/

  • encode-adts.agda
  • unbound-vars.agda

7/

  • subst.agda

./Bend/Compile/

8/

  • book-to-hvm.agda

./Base/AVLTree/Delete/

14/

  • delete-go.agda

23/

  • delete-maximum-.agda

9/

  • delete-maximum.agda

./Base/Parser/Examples/LambdaTerm/Test/

9/

  • y-combinator.agda

./HVM/Parser/

11/

  • parse-net-.agda
  • parse-term-.agda

12/

  • parse-net.agda

14/

  • parse-term.agda

9/

  • parse-redex.agda

./HVM/Run/State/

14/

  • show.agda

9/

  • State.agda
  • boot.agda

./Base/JSON/Test/

10/

  • parse-null.agda
  • parse-string.agda

11/

  • parse-bool.agda

13/

  • parse-object.agda

14/

  • parse-array.agda

15/

  • parse-number.agda

./Imp/Backend/Cuda/

11/

  • grid-to-cuda.agda

./Base/Network/

12/

  • ALL.agda

./UG/SIPD/

13/

  • draw.agda

88/

  • Main.agda

./Bend/Parser/Fun/

14/

  • parse-book-.agda
  • parse-pattern-.agda

15/

  • parse-def-sig-.agda

17/

  • parse-term-.agda

18/

  • parse-def-sig.agda
  • parse-rule-lhs.agda

23/

  • parse-pattern.agda
  • parse-type-term.agda

24/

  • parse-fn-def-.agda

26/

  • parse-adt.agda

30/

  • parse-fn-def.agda

33/

  • parse-book.agda

42/

  • parse-term.agda

./Bend/Load/

16/

  • load-book.agda

./Bend/Compile/Test/

19/

  • book-to-hvm.agda

./HVM/

19/

  • Main.agda

./Bend/Compile/BendToNet/

22/

  • book-to-nets.agda

./Bend/Fun/Book/Test/

23/

  • show.agda

./Imp/Eval/

31/

  • eval-expr.agda

./Base/

34/

  • ALL.agda
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment