- 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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import cats.Monad | |
import cats.syntax.all.* | |
object Validation: | |
enum ValidationLevel: | |
case Mandatory | |
case Desirable | |
case Optional |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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() |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{- | |
FATA @ UoG Uma Zalakain | |
-------------------------------------------- | |
Theorem Proving with Dependent Types in Agda | |
-} | |
{- | |
Agda | |
is a "pure dependently typed total functional programming language" |