ComFreek

From Coq Require Import ssreflect ssrfun ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Fixpoint plus' (n m: nat): nat := match n with | S n' => plus' n' (S m) | 0 => m end.

Lemma helper_lemma: forall n m, plus' n (S m) = S (plus' n m).
Proof.
  elim => // [n IHn m].

ComFreek

1. add import io.circe.generic.auto._ where you use the auto-derived JSON encoders and decoders (don't import at file-level, but instead on object/class-level!)

   • e.g. in a file Datastructures.scala you declare sealed case Data(x: Int) and in Usage.scala you have

     import io.circe.Json  // needed?
     
     // for .asJson methods to be "added" to classes for which implicit encoders exist
     import io.circe.syntax._ 
     

object Usage {

ComFreek

Every time I wanted to convert nat to string in the most obvious manner (i.e. decimal), I had to search >= 10min in the libraries for the right function calls!

Require Import Numbers.DecimalString.
Require Import Numbers.DecimalNat.

Definition nat_to_string (n: nat) := NilZero.string_of_uint (Decimal.rev (Unsigned.to_lu n)).
Compute (nat_to_string 0).   (*  "0" *)
Compute (nat_to_string 42). (* "42" *)

ComFreek

The Future of Typesetting Manifesto

Goal

• Collect design decisions and criteria for a next-gen typesetting languaeg
• Learn from past mistakes of (La)TeX, Markdown, and other products

Recipients

Everyone who is interested in good design of a TeX-successor. With some points, it might be required to have a bit of background in type theories.

ComFreek

Compilation of Syntax Highlighting Solutions used in Major Software Products

GRLs (generalized regex lexers; made-up name) are a common lexer type which are represented by a

• deterministic state-based finite automaton with regex at eges (similar to generalized non-det. finite automaton),
• such that edges can not only transition to a new state but also push or pop multiple states and also issue/yield token types (e.g. "keyword", "string", "punctuation").
• additionally, the set of outgoing edges for a state is actually ordered ("list of rules"; what matches first, is gone first),
• and you can also import the rule lists from other states (e.g. have a common "comment rule list")

(Is there a formal name for it? See also , a spec that apparently never took off)

ComFreek

Inductive pl : Prop := disj: pl -> pl -> pl.

Definition context := pl -> Prop.

Reserved Notation "Gamma '|-' f" (at level 65).
Inductive plDerivable : context -> pl -> Prop :=

  disjElim: forall ctx (p q r: pl),
       ctx |- disj p q
    -> (ctx |- p -> ctx |- r)

ComFreek

# Block liking of content
facebook.com##a[role=button]:has-text(Like)

# Block creation of own content
facebook.com##a[role=button]:has-text(Reply)
facebook.com##div[aria-label="Write a reply"]
facebook.com##div[aria-label="Write a comment..."]
facebook.com##div[aria-label="Create a post"]

facebook.com##form.commentable_item form

ComFreek

// Only works with System V AMD64 ABI (e.g. if you compile your code to 64-bit targetting Linux)

typedef uint64_t fun_arg_t;

/**
 * Call a function with given arguments.
 *
 * This requires System V AMD64 ABI compilation for this function as well as the called function.
 *
 * @param fun Pointer to the function

ComFreek

Cypher query to count the number of wcc's of size >= 2:

CALL algo.unionFind.stream('User', null, {})
YIELD nodeId, setId
WITH setId, count(*) AS componentSize
WHERE componentSize >= 2
RETURN count(*) as numberOfComponentsOfSize2OrGreater

ComFreek

TypeScript unit tests

1. npm install mocha chai ts-node typescript @types/mocha @types/chai --save-dev

2. Edit your package.json to include:

    scripts: {
     "test": "node --harmony node_modules/mocha/bin/mocha --harmony -r ts-node/register *.spec.ts"
   }