{{ message }}

Instantly share code, notes, and snippets.

# Uma Zalakain umazalakain

Created Apr 12, 2021
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
Created Apr 2, 2021
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()
Last active Mar 21, 2021

• 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
Created Jan 25, 2021
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
Last active Jan 11, 2021
View DepTypes.agda
 {- FATA @ UoG Uma Zalakain -------------------------------------------- Theorem Proving with Dependent Types in Agda -} {- Agda is a "pure dependently typed total functional programming language"