Binary-Song

Syntax	Explanation
#eval	evaluates
#check	checks type (for functions, wrap in parentheses)
t.f arg1 arg2	With type T and function T.f (arg1: X) (argt: T) (arg2: Y), this means T.f arg1 t arg2 (the t goes to whichever param that has type T, others laid out in order)
def lean : String := "Lean"	defines value
def add1 (n : Nat) : Nat := n + 1	defines function
def Str : Type := String	defines type (not reducible)
abbrev Str : Type := String	defines alias (reducible)
structure Point where x : Float y : Float deriving Repr	defines structure with derived code

Binary-Song

include mem.h to enable memory check in this file. 'memory_leaks' variable indicates how many memories are unfreed.

Binary-Song

git config --global http.proxy 'http://127.0.0.1:1080'
git config --global https.proxy 'https://127.0.0.1:1080'

取消代理：

git config --global --unset http.proxy
git config --global --unset https.proxy

Binary-Song

ssh-rsa AAAAB3NzaC1yc2EAAAADAQABAAABAQC5SiRCD/Rbsq6QkCSghhczBQnK2bAU+Jgka+DadelpOgaUJNZrxyEhzuoOY+6ycDjDwaDHBod5qGq3uFeBk58y6xcA/CX6rG/hnzkF9Y+kCJe0KBb6HwvWxBsEjGU16QHNBX6DMI0TzqhZT/oVQz+h9BESdlshEOiWuQGSINGT9A1IeJr/coS/TKdrJY51T8U5q/baXhCkG0PjO/of/neGCOZFt6vsqn1Fjfr0JUiEuOw9g4ElrtAjKV60fu1upahAh6+q3yMw+o0m7ZPpMyksNHlOoMvDgbFAj0C/HA833CeGCc0Jyq1eKIlYDlrOi2S4+l2D7riasXvlN/DdK5aV BinarySong

Binary-Song

{
    "version": "0.2.0",
    "configurations": [
        {
            "name": "gdb debug",
            "type":"cppdbg",
            "request": "launch",
            "program": "${workspaceFolder}/build/${fileBasenameNoExtension}.exe",
            "args": [],
            "stopAtEntry": false,

Binary-Song

{ 
    "version": "0.2.0",
    "configurations": [
        {
            "name": "Windows CMake Launch",
            "type": "cppvsdbg",
            "request": "launch",
            "program": "${command:cmake.launchTargetPath}",
            "args": [],
            "stopAtEntry": false,