Skip to content

Instantly share code, notes, and snippets.


Block or report user

Report or block MaiaVictor

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
MaiaVictor / Church
Created May 26, 2019 — forked from takanuva/Church
Conversion between Scott encoding and Church endocing for naturals in CoC
View Church
\/(N: *) ->
\/(z: N) ->
\/(s: N -> N) ->
MaiaVictor / linear.agda
Created Mar 26, 2019 — forked from gallais/linear.agda
Raw linear terms
View linear.agda
open import Data.Nat.Base
open import Data.Vec
open import Data.Bool.Base using (Bool; false; true)
open import Data.Product
m n :
b : Bool
Γ Δ Ξ T I O : Vec Bool n
MaiaVictor / UntypedLambda.agda
Created Mar 1, 2019 — forked from gallais/UntypedLambda.agda
Interpreting the untyped lambda calculus in Agda
View UntypedLambda.agda
{-# OPTIONS --copatterns #-}
module UntypedLambda where
open import Size
open import Function
data Delay (A : Set) (i : Size) : Set where
MaiaVictor /
Created Apr 5, 2018 — forked from zmactep/
Number encodings

Alternative to the Church, Scott and Parigot encodings of data on the Lambda Calculus.

When it comes to encoding data on the pure λ-calculus (without complex extensions such as ADTs), there are 3 widely used approaches.

Church Encoding

The Church Encoding, which represents data structures as their folds. Using Caramel’s syntax, the natural number 3 is, for example. represented as:

0 c0 = (f x -> x)
1 c1 = (f x -> (f x))
2 c2 = (f x -> (f (f x)))
MaiaVictor / .emacs
Created Mar 16, 2018 — forked from nkaretnikov/.emacs
Agda .emacs
View .emacs
(add-to-list 'load-path "~/.emacs.d/evil")
(require 'evil)
(evil-mode 1)
;; Highlight matching parens.
(show-paren-mode 1)
;;; No tabs.
(setq-default ident-tabs-mode nil)
(setq-default tab-width 4)
You can’t perform that action at this time.