2024-10-13 08:00:44 +02:00
|
|
|
import common/math-phrases
|
|
|
|
|
2024-04-27 21:38:06 +02:00
|
|
|
block auto start
|
|
|
|
for thmenv <- @⟨lemma,theorem,corollary,definition⟩
|
|
|
|
string @thmenv
|
|
|
|
snip
|
|
|
|
#@thmenv$|1⟨(name: "$1"),$1⟩[
|
|
|
|
$0
|
|
|
|
]
|
|
|
|
|
2024-05-07 03:03:10 +02:00
|
|
|
for proofenv <- @⟨proof,solution,exercise,example⟩
|
2024-04-27 21:38:06 +02:00
|
|
|
string @proofenv
|
|
|
|
snip
|
|
|
|
#@proofenv$|1⟨$1,(name: "$1")⟩[
|
|
|
|
$0
|
|
|
|
]
|
|
|
|
|
|
|
|
string dm
|
|
|
|
name display math
|
|
|
|
snip
|
|
|
|
$
|
|
|
|
$0
|
|
|
|
$
|
|
|
|
|
|
|
|
block auto
|
|
|
|
string ccf
|
|
|
|
name continuously differentiable function
|
|
|
|
snip $C^1$
|
|
|
|
|
|
|
|
string ftdef
|
|
|
|
name function type definition
|
|
|
|
snip $$1 : $2 → $3$ $0
|
|
|
|
|
|
|
|
block auto
|
|
|
|
string tdif
|
|
|
|
name total derivative
|
|
|
|
snip (dif $1) / (dif $2) $0
|
|
|
|
|
|
|
|
string pdif
|
|
|
|
name partial derivative
|
|
|
|
snip (diff $1) / (diff $2) $0
|
|
|
|
|
|
|
|
string dint
|
|
|
|
name definite integral
|
|
|
|
snip ∫_$|1⟨$1,(-∞$1)⟩^$|2⟨$2,∞$2⟩ $3 dif $0
|
|
|
|
|
|
|
|
for limtarget <- @⟨anything,zero,infinity,negative infinity⟩
|
|
|
|
for prefix <- @⟨@limtarget:,z,i,n⟩
|
|
|
|
for limtargetsymbol <- @⟨@limtarget:$2,0,∞,-∞⟩
|
|
|
|
string @prefix⋄lim
|
|
|
|
name limit to @limtarget
|
|
|
|
snip lim_($1 → @limtargetsymbol) $0
|
|
|
|
|
|
|
|
for operator <- @⟨eq,neq,defas,leq,geq,lt,gt,iip,iib,iff⟩
|
|
|
|
for symbol <- @⟨@operator:=,≠,≔,≤,≥,<,>,⟹,⟸,⟺⟩
|
|
|
|
|
|
|
|
abbr @operator @symbol
|
|
|
|
|
|
|
|
string a@operator
|
|
|
|
name align at @operator
|
|
|
|
snip &@symbol $0
|
|
|
|
|
|
|
|
block start
|
|
|
|
string al@operator
|
|
|
|
name aligned @operator
|
|
|
|
snip
|
|
|
|
\ $1 &@symbol $2
|
|
|
|
$0
|
|
|
|
|
|
|
|
string cr@operator
|
|
|
|
name start with @operator
|
|
|
|
snip \ &@symbol $0
|
2024-05-07 03:03:10 +02:00
|
|
|
|
|
|
|
block never
|
|
|
|
pattern (.*)e@⟨t(%a),(%d)⟩
|
|
|
|
name auto exponent
|
|
|
|
snip @0^@1 $0
|
|
|
|
|
|
|
|
pattern (.*)so(%a)
|
|
|
|
name auto subscript
|
|
|
|
snip @0_@1 $0
|
|
|
|
|
|
|
|
pattern ([%a]+)(%d)
|
|
|
|
name auto digt subscript
|
|
|
|
snip @0_@1 $0
|
|
|
|
|
|
|
|
string ss
|
|
|
|
name subscript
|
|
|
|
snip _{$1} $0
|
|
|
|
|
|
|
|
string ee
|
|
|
|
name exponent
|
|
|
|
snip ^($1) $0
|
|
|
|
|
|
|
|
pattern (%a)(.)pp
|
|
|
|
name auto function call
|
|
|
|
snip @0(@1) $0
|
|
|
|
|
|
|
|
pattern (%a)d(.)p
|
|
|
|
name auto derivative call
|
|
|
|
snip @0'(@1) $0
|
|
|
|
|
|
|
|
pattern (%a)i(.)p
|
|
|
|
name auto preimage call
|
|
|
|
snip @0^(-1)(@1) $0
|
|
|
|
|
|
|
|
block !word
|
|
|
|
abbr .inv ^(-1)
|
|
|
|
abbr .neg _-
|
|
|
|
abbr .pos _+
|