Skip to content

Instantly share code, notes, and snippets.

View arithexpr2
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
View typelevel-deBruijn-scala
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 /
Last active Mar 21, 2021
Uma's RISE 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
View lambdacalc.scala
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
View DepTypes.agda
FATA @ UoG Uma Zalakain
Theorem Proving with Dependent Types in Agda
is a "pure dependently typed total functional programming language"