tzemanovic / plfa

guest › [sign in] [explore]

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

mode name

drwxr-xr-x EvalContexts/

drwxr-xr-x Frames/

drwxr-xr-x denotational/

drwxr-xr-x extra/

drwxr-xr-x fixpoint/

drwxr-xr-x fixpoint-old/

drwxr-xr-x fresh/

drwxr-xr-x qtt/

drwxr-xr-x stlc/

drwxr-xr-x variants/

-rw-r--r-- 842Inference.agda

-rw-r--r-- DeMorgan.lagda.md

-rw-r--r-- Inherent.lagda

-rw-r--r-- Issue488.agda

-rw-r--r-- KovacsSTLCnorm.agda

-rw-r--r-- LambdaReduction.lagda.md

-rw-r--r-- Modules.lagda.md

-rw-r--r-- Pure.lagda

-rw-r--r-- PureConor.lagda

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

-rw-r--r-- Reflection.lagda.md

-rw-r--r-- Subtyping-comments.lagda.md

-rw-r--r-- Subtyping-phil.lagda.md

-rw-r--r-- Subtyping.lagda.md

-rw-r--r-- bin-suggestion.lagda.md

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

-rw-r--r-- iso-exercise.lagda

-rw-r--r-- plfa-extra.agda-lib