Jiří Beneš jiribenes

## Compiler.agda
{-# OPTIONS --without-K --safe #-}

module Compiler where

data List (A : Set) : Set where
  [] : List A
  _∷_ : A → List A → List A

infixr 5 _∷_
{-# BUILTIN LIST List #-}

## keybase.md

      
        
          
            
              
              1 file
            
          
          
            
              
              0 forks
            
          
          
            
              
              0 comments
            
          
          
            
              
              0 stars
            
          
        
        
          
              
          
          
            
                jiribenes
                / keybase.md
            
            
              Created
              March 18, 2017 13:49
            
          
        
      
        
  
      
    Keybase proof

I hereby claim:

I am jiribenes on github.
I am jiribenes (https://keybase.io/jiribenes) on keybase.
I have a public key whose fingerprint is 5E34 7775 E880 5402 3872  62BD D5F9 58FA CE02 3AF5

To claim this, I am signing this object:
	{-# OPTIONS --without-K --safe #-}

	module Compiler where

	data List (A : Set) : Set where
	[] : List A
	_∷_ : A → List A → List A

	infixr 5 _∷_
	{-# BUILTIN LIST List #-}