anton0xf

Require Import Arith.
Require Import List.
Import ListNotations.

Check 1 :: 2 :: nil.
Check [1; 2].

Fixpoint make_payrolls_rec (d a: nat) (r: list (nat * nat)) :=
  match d with
  | 0 => r

anton0xf

(*** oveloaded lemmas *)
(** Lambda World 2018 - How to make ad hoc proof automation less ad hoc
    by Aleksandar Nanevski
    https://www.youtube.com/watch?v=yFIaP1YCcxQ&t=36s *)

Require Import Bool.
Require Import String.
Require Import FunctionalExtensionality.
Require Import List.
Import ListNotations.

anton0xf

Require Import Nat.

Theorem add_comm: forall n m: nat, n + m = m + n.
Proof.
  induction n as [|n' IH].
  - (** n = O *)
    intro m. simpl. rewrite <- plus_n_O. reflexivity.
  - (** n = S n' *)
    intro m. simpl. rewrite <- plus_n_Sm. rewrite IH. reflexivity.
Qed.

anton0xf

module NextBiggerSpec (spec) where

import Test.Hspec
import Test.QuickCheck
import NextBigger (nextBigger)
import Data.List (sort,unfoldr)
import Data.Tuple (swap)
import Data.Maybe (isJust,fromJust)

spec :: Spec

anton0xf

import itertools


class Cons:
    def __init__(self, head, tail_fn):
        self.head = head
        self._tail_fn = tail_fn
        self._tail = None

    def tail(self):

anton0xf

#lang racket
(define (fib n)
  (if (< n 2) n
      (+ (fib (- n 1))
         (fib (- n 2)))))
(time (fib 35))
; cpu time: 5219 real time: 5138 gc time: 747
; => 9227465

(require memo)

anton0xf

import org.junit.jupiter.api.Assertions;
import org.junit.jupiter.api.Test;

import java.util.LinkedList;
import java.util.List;
import java.util.ListIterator;

public class InsertBeforeTest {
    private void insertBefore(int before, int val, ListIterator<Integer> iter) {
        while(iter.hasNext()) {

anton0xf

;; run it by command
;; $ emacs -Q --script test2.el

(setq line "asdf qwer")
(add-face-text-property 0 4 'a t line)
(add-face-text-property 0 5 'b t line)
(print line)
;; #("asdf qwer" 0 4 (face (a b)) 4 5 (face b))

(setq word (substring line 0 4))

anton0xf

;; run it by command
;; $ emacs -Q --script test-add-face-text-property.el
(setq line "asdf qwer")
(add-face-text-property 0 4 'a t line)
(add-face-text-property 0 4 'a t line)
(print line)
;; #("asdf qwer" 0 4 (face a))

(add-face-text-property 0 5 'b t line)
(add-face-text-property 0 5 'b t line)

anton0xf

(defun company--begin-new ()
  (let (prefix c)
    (cl-dolist (backend (if company-backend
                            ;; prefer manual override
                            (list company-backend)
                          company-backends))
      (setq prefix
            (if (or (symbolp backend)
                    (functionp backend))
                (when (company--maybe-init-backend backend)