tzemanovic / plfa

guest › [sign in] [explore]

{/} code [~] changes [>] discussions [*] jobs

mode name

-rw-r--r-- Addition.agda

-rw-r--r-- Basics-old.lagda

-rw-r--r-- Basics.lagda

-rw-r--r-- CPP.lagda

-rw-r--r-- Chain.lagda

-rw-r--r-- Collections-backup.lagda

-rw-r--r-- Collections-setoid.lagda

-rw-r--r-- Darais.agda

-rw-r--r-- DaraisPhoas.agda

-rw-r--r-- DeBruijn-agda-list-2.lagda

-rw-r--r-- DeBruijn-agda-list-3.lagda

-rw-r--r-- DeBruijn-agda-list-4.lagda

-rw-r--r-- DeBruijn-agda-list.lagda

-rw-r--r-- DeBruijn2.lagda

-rw-r--r-- DecidableBroken.agda

-rw-r--r-- DecidableExtra.lagda

-rw-r--r-- DecidableFixed.agda

-rw-r--r-- Denotational.lagda

-rw-r--r-- Dummy.agda

-rw-r--r-- Equivalence-old.lagda

-rw-r--r-- Eta.agda

-rw-r--r-- Even.agda

-rw-r--r-- EvenOdd.agda

-rw-r--r-- EvenOdd2.agda

-rw-r--r-- EvenOdd3.agda

-rw-r--r-- Everything.agda

-rw-r--r-- Exercises.lagda

-rw-r--r-- Extra.lagda

-rw-r--r-- FreshId-backup.lagda

-rw-r--r-- FreshIdConor.lagda

-rw-r--r-- FreshUnstuck-backup.lagda

-rw-r--r-- Gentzen.lagda

-rw-r--r-- Head.agda

-rw-r--r-- IdMap.lagda

-rw-r--r-- InferenceOld.lagda

-rw-r--r-- Isomorphisms.agda

-rw-r--r-- Lambda-new.lagda

-rw-r--r-- LambdaSyntax.lagda

-rw-r--r-- Lexical.lagda

-rw-r--r-- Liftable.agda

-rw-r--r-- Lists-backup.lagda

-rw-r--r-- Lists.lagda.md

-rw-r--r-- Logic.lagda

-rw-r--r-- Membership.agda

-rw-r--r-- Mendler.agda

-rw-r--r-- Module.agda

-rw-r--r-- ModuleInfix.agda

-rw-r--r-- Monus.agda

-rw-r--r-- Mutual.agda

-rw-r--r-- Mutual2.agda

-rw-r--r-- Nat.agda

-rw-r--r-- Negation-notes.lagda

-rw-r--r-- OldSubstitution.lagda

-rw-r--r-- PHOAStoEXP.agda

-rw-r--r-- Preorder.agda

-rw-r--r-- Preorder.lagda

-rw-r--r-- PropertiesDec.lagda

-rw-r--r-- Raw-deadend.lagda

-rw-r--r-- Raw-deadend2.lagda

-rw-r--r-- Reasoning.agda

-rw-r--r-- Reasoning2.agda

-rw-r--r-- Rec1.agda

-rw-r--r-- Rec2.agda

-rw-r--r-- Reduction.lagda

-rw-r--r-- Rev.agda

-rw-r--r-- RewriteWTF.agda

-rw-r--r-- SmallInherent.lagda

-rw-r--r-- Stable.agda

-rw-r--r-- StreamLambdaProp.lagda

-rw-r--r-- Streams.lagda

-rw-r--r-- Subset.lagda

-rw-r--r-- SystemF.lagda

-rw-r--r-- TakeDropBool.agda

-rw-r--r-- TakeDropDec.agda

-rw-r--r-- TakeDropDecTest.agda

-rw-r--r-- Typed-backup.lagda

-rw-r--r-- Typed-string.lagda

-rw-r--r-- Typed-wf-deadend.lagda

-rw-r--r-- Typed.lagda

-rw-r--r-- Typed.lagda.broken

-rw-r--r-- TypedDB-backup.lagda

-rw-r--r-- TypedFresh-away.lagda

-rw-r--r-- TypedFresh-backup.lagda

-rw-r--r-- Ulf.agda

-rw-r--r-- Untyped-CBV.lagda

-rw-r--r-- UntypedDB.lagda

-rw-r--r-- Value.agda

-rw-r--r-- outline.lagda