Нет времени объяснять, переходим сразу к делу.
Доказывать теоремы мы будем, используя интерактивные пруверы Isabelle или Lean 3. Примеры приводятся для каждого прувера, для решения задач же можно использовать любой из них.
s:+: ConjugateAdd :g | |
s:-: NegateSubtract :g | |
s:×: SignMultiply :g | |
s:÷: ReciprocalDivide :g | |
s:⋆: ExponentialPower :g | |
s:√: SquareRootRoot :g | |
s:⌊: FloorMinimum :g | |
s:⌈: CeilingMaximum :g | |
s:∧: SortUpAnd :g | |
s:∨: SortDownOr :g |
s:∘.: outerProduct_ :g | |
s:+: ConjugatePlus :g | |
s:-: NegateMinus :g | |
s:×: DirectionTimes :g | |
s:÷: ReciprocalDivide :g | |
s:⌊: FloorMinimum :g | |
s:⌈: CeilingMaximum :g | |
s:|: MagnitudeResidue :g | |
s:*: ExponentialPower :g | |
s:⍟: NatualLogarithmLogarithm :g |
# SSE to BQN dictonary | |
# This is an implementation of SSE SIMD intristics in BQN. The purpose of it | |
# is understanding: it's a look at SIMD instructions from an array programmer POV. | |
# There are limit of what you can can represent in a programming language without | |
# losing clarity. Bit hackery is one of such features. So instead of converting | |
# from floats to bits and back, we just assume that the data *already* is | |
# represented the way we need. |
# APL keyboard | |
<Multi_key> <space> <z> : "⊂" | |
<Multi_key> <space> <Z> : "⊆" | |
<Multi_key> <space> <x> : "⊃" | |
<Multi_key> <space> <c> : "∩" | |
<Multi_key> <space> <v> : "∪" | |
<Multi_key> <space> <b> : "⊥" | |
<Multi_key> <space> <n> : "⊤" | |
<Multi_key> <space> <less> : "⍝" | |
<Multi_key> <space> <comma> : "⍪" |
There are some articles you want to read first:
Nix Flakes is currently an experimental feature, so this tutorial assumes that you are using the unstable
channel.
{ | |
PendingTask | EndedTask | WaitingTask | RecurringParrentTask | RecurringChildTask | |
... | |
} | |
Task :: { | |
status: Status | |
uuid: Uuid | |
entry: Date | |
description: string |
Flamegraphs can help to optimize the program a lot. So let's create one!
unwind
enabledperf record -F 99 --call-graph dwarf -- ‹your program›
perf script | stackcollapse-perf.pl > out.folded