玩火 niltok

## gcmformojo架设教程.md

      
              1 file
            
          
              11 forks
            
          
              14 comments
            
          
              66 stars
            
          
                kotomei
                / gcmformojo架设教程.md
            
            
              Last active
              February 22, 2022 11:04
            
          
  title
  date
  tags
  
  
  GCMForMojo 的部署与设置
  2017-01-21 11:07:03 -0800
  
  
  GCM
  Android
  
  
2017年2月6日更新：完善部分内容，更新内容

2017年2月8日更新：发现自己脑抽少写了一步较为关键的步骤，赶紧补上orz，连带解决笔误


## encodings.md

      
              1 file
            
          
              4 forks
            
          
              2 comments
            
          
              16 stars
            
          
                zmactep
                / encodings.md
            
            
              Created
              August 20, 2017 13:08
            
              
                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 -&gt; (f (f x)))


## Synthesis.agda
{-# OPTIONS --prop --without-K --safe #-}

module Synthesis where

-- Utilities
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.Nat using (zero; suc; _+_) renaming (Nat to ℕ)

infixl 8 _∧_ _×_
	{-# OPTIONS --prop --without-K --safe #-}

	module Synthesis where

	-- Utilities
	open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
	open import Agda.Builtin.Equality using (_≡_; refl)
	open import Agda.Builtin.Nat using (zero; suc; _+_) renaming (Nat to ℕ)

	infixl 8 _∧_ _×_