umazalakain

import cats.Monad
import cats.syntax.all.*

object Validation:

  enum ValidationLevel:
    case Mandatory
    case Desirable
    case Optional

umazalakain

open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
open import Data.Fin.Base as Fin using (Fin; zero; suc)
open import Data.Vec.Base as Vec using (Vec; []; _∷_)

module Syntax where

module Lambda where
  -- The variable keyword lets you introduce conventions
  -- E.g. if n is mentioned anywhere without being bound it refers to a ℕ
  variable

umazalakain

open import Function using (_∘_)
open import Data.Integer.Base as ℤ using (ℤ)
open import Data.Fin.Base as Nat using (Fin; zero; suc)
open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
open import Data.Vec.Base as Vec using (Vec; []; _∷_)
open import Data.Maybe.Base as Maybe using (Maybe; nothing; just)

private variable n m l : ℕ

data UnOp : Set where

umazalakain

object DeBruijn {
  sealed trait Nat
  sealed trait Z           extends Nat
  sealed trait S[n <: Nat] extends Nat

  sealed trait Fin[n <: Nat]
  case class FZ[n <: Nat]()           extends Fin[S[n]]
  case class FS[n <: Nat](n : Fin[n]) extends Fin[S[n]]

  val here : Fin[S[S[Z]]] = FZ()

umazalakain

Tasks

• rise traversals
• dpia traversals
• index translation
  • some expressions do not get translated
  • some indices are missing from the path
• rise primitive documentation
  • create issue re. identifier naming before merging
• dpia primitive documentation

umazalakain

object LambdaCalculus {
  sealed trait Type
  case class Arrow[S <: Type, T <: Type]() extends Type
  case class Base() extends Type

  sealed trait Ctx
  case class Nil() extends Ctx
  case class Cons[X <: Type, XS <: Ctx]() extends Ctx

umazalakain

{-
FATA @ UoG                      Uma Zalakain
--------------------------------------------
Theorem Proving with Dependent Types in Agda
-}


{-
Agda
  is a "pure dependently typed total functional programming language"