ttesmer

{-# LANGUAGE TypeSynonymInstances #-}
data Dual d = D Float d deriving Show
type Float' = Float

diff :: (Dual Float' -> Dual Float') -> Float -> Float'
diff f x = y'
  where D y y' = f (D x 1)

class VectorSpace v where
  zero  :: v

SharkPlush

I have a website now that includes a more dumbed down but straight forward version of this guide that isnt basied towards Arch Linux but considers most distros. https://linuxguidance.net/improve-battery-and-optimize-your-linux-laptop/

Everything I do in this guide is mostly taken from the Arch Wiki, and is for Arch Linux, obviously this can probably be applied to other Linux distributions especially Arch based ones, this guide is for people who want a laptop with similar effciency they had on Windows or MacOS. I hate the excuse of having to compromise on Linux to have good battery or thermals on laptops.

Please think of this guide as more of a starting point, if you're serious about fully optimizing your laptop research your laptop and the hardware inside of it as that can get you even further down the rabbit hole.

This guide assumes you have a relatively modern laptop with at least an SSD from the factory, if you don't, don't worry you can still probably follow this guide perfectly, if you have a 32-b

wenkokke

Tactics in Agda

This gist is my attempt to list all projects providing proof automation for Agda.

Glossary

When I say tactic, I mean something that uses Agda's reflection to provide a smooth user experience, such as the solveZ3 tactic from Schmitty:

_ : ∀ (x y : ℤ) → x ≤ y → y ≤ x → x ≡ y
_ = solveZ3

wavezhang

wget -c --no-cookies --no-check-certificate --header "Cookie: oraclelicense=accept-securebackup-cookie"  https://download.oracle.com/otn-pub/java/jdk/12.0.2+10/e482c34c86bd4bf8b56c0b35558996b9/jdk-12.0.2_linux-x64_bin.tar.gz

kevinkindom

Python Socket 编程详细介绍

Python 提供了两个基本的 socket 模块：

• Socket 它提供了标准的BSD Socket API。
• SocketServer 它提供了服务器重心，可以简化网络服务器的开发。

下面讲解下 Socket模块功能。

Socket 类型

nikAizuddin

;          1         2         3         4         5         6         7
;01234567890123456789012345678901234567890123456789012345678901234567890
;=======================================================================
;+---------------------------------------------------------------------+
;|                                                                     |
;| Example using brk() system call for dynamic memory allocations.     |
;|                                                                     |
;| DON'T CONFUSE that brk() used in C Function is different with brk() |
;| systemcall (systemcall 45 for x86 ASM).                             |
;|                                                                     |

chaitanyagupta

Reader Macros in Common Lisp

This post also appears on lisper.in.

Reader macros are perhaps not as famous as ordinary macros. While macros are a great way to create your own DSL, reader macros provide even greater flexibility by allowing you to create entirely new syntax on top of Lisp.

Paul Graham explains them very well in [On Lisp][] (Chapter 17, Read-Macros):

The three big moments in a Lisp expression's life are read-time, compile-time, and runtime. Functions are in control at runtime. Macros give us a chance to perform transformations on programs at compile-time. ...read-macros... do their work at read-time.

grenade

#!/bin/bash

mkdir -p ~/.ssh

# generate new personal ed25519 ssh keys
ssh-keygen -o -a 100 -t ed25519 -f ~/.ssh/id_ed25519 -C "rob thijssen <rthijssen@gmail.com>"
ssh-keygen -o -a 100 -t ed25519 -f ~/.ssh/id_robtn -C "rob thijssen <rob@rob.tn>"

# generate new host cert authority (host_ca) ed25519 ssh key
# used for signing host keys and creating host certs

drj42

Org-mode Org-mode Reference Card

Org mode reference card

Created from the plain text reference card on orgmode.org Download this file, and open it in Emacs org-mode!