AlecsFerra

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

import Data.Data (Proxy (Proxy))
import Data.Kind (Type)
import Text.Printf (printf)

AlecsFerra

module AxiomK where

open import Relation.Binary.PropositionalEquality using (_≡_)
open _≡_

-- All the equality proofs are the same ⁾
-- Unless we use the `--without-K` option ⁾
same-≡ : ∀ {l} {A : Set l} {a b : A} → (p₁ p₂ : a ≡ b) → p₁ ≡ p₂
same-≡ refl refl = refl

AlecsFerra

module RewriteAbuse where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)

+-swap : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap m n p rewrite (sym (+-assoc m n p))
             |       (+-comm m n)
             |       (+-assoc n m p)

AlecsFerra

;; Some proofs about pairs
;; ∀ a b c. a = b → (a, c) = (b, c)
(claim a=b→ac=bc
  (Π ([T U]
      [K U]
      [a T]
      [b T]
      [c K]
      [_ (= T a b)])
    (= (Pair T K) (cons a c) (cons b c))))

AlecsFerra

; last
(claim last
  (Π ((Of U)
      (many-1 Nat)
      (vec (Vec Of (add1 many-1))))
    Of))
(define last
  (λ (Of many-1 vec)
    ((ind-Nat many-1
      (λ (many-1)

AlecsFerra

Keybase proof

I hereby claim:

• I am alecsferra on github.
• I am alecsferra (https://keybase.io/alecsferra) on keybase.
• I have a public key ASAJE6eEkoGFeGf_LAF1ZhaduDhazfmJRUIMvemvGYDItQo

To claim this, I am signing this object:

AlecsFerra

print("""
main = do
    print "Welcome to my addition calculator :)"
    a <- getLine
    b <- getLine
    print $ add (read a) (read b)
""")

for i in range(1000):
    for j in range(1000):

AlecsFerra

import Data.Char
import Control.Applicative
import Data.Either
import Data.Tuple.Extra

type Position      = (Int, Int)
type ParserInput   = (Position, String)
type ParseError    = (Position, [String])
type Parsed a      = (Position, String, a)
type ParseResult a = Either ParseError (Parsed a)

AlecsFerra

public class EnterpriseCoreApplication {
    public static void main(String... args) {
        for (java.lang.Integer i = new java.lang.Integer(0); i.compareTo(new java.lang.Integer(69)) < 0; i = EnterpriseCoreApplication.IntegerIncrement(i)) {
            System.out.println(i.toString());
        }
    }
    
    public static java.lang.Integer IntegerIncrement(final java.lang.Integer inputInteger) {
        if (inputInteger.compareTo(Integer.MAX_VALUE) == 0) {
            throw new RuntimeException("Business supercazzola enterprise i32 overflow");

AlecsFerra

:- module parser.

:- interface.

:- import_module char, list, value.

:- pred top_level_expression(lisp_value::out, list(char)::in, list(char)::out) is semidet.

:- implementation.