Comfy Agda Dev Environment [hca/H00D.lagda]

    What we need

    • an agda installation
    • a nice text editor (Neovim + Cornelis)
    • literate programming support

    Working with Cornelis

    We will assume two Types A and B.

    data A : Type where
  a1 : A
  a2 : A

postulate
  B : Type

    Load agda files with :CornelisLoad

    Goals {!!}, :CornelisTypeContextInfer

    someFunc : A -> B
someFunc a = {!!}

    Split cases with :CornelisMakeCase.

    -- switch : A -> A
-- switch a1 = a2
-- switch a2 = a1

switch : A -> A
switch a = {!!}

    What is switch a1? Normalize expressions with :CornelisNormalize

    Links