Skip to content

Instantly share code, notes, and snippets.

MaiaVictor

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
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) ->
N
@MaiaVictor
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
variable
m n :
b : Bool
Γ Δ Ξ T I O : Vec Bool n
@MaiaVictor
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
mutual
data Delay (A : Set) (i : Size) : Set where
@MaiaVictor
MaiaVictor / encodings.md
Created Apr 5, 2018 — forked from zmactep/encodings.md
Number encodings
View encodings.md

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
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.