Skip to content

Instantly share code, notes, and snippets.

View jwiegley's full-sized avatar

John Wiegley jwiegley

View GitHub Profile
(defcustom erc-foolish-content '()
"Regular expressions to identify foolish content.
Usually what happens is that you add the bots to
`erc-ignore-list' and the bot commands to this list."
:group 'erc
:type '(repeat regexp))
(defun erc-foolish-content (msg)
"Check whether MSG is foolish."
(erc-list-match erc-foolish-content msg))
((tool-bar-position . top)
(parent-id)
(explicit-name)
(display . "Mac")
(icon-name)
(window-id . "105553126770080")
(top . 0)
(left . 0)
(buried-buffer-list #<buffer *Backtrace*> #<buffer .newsrc-dribble> #<buffer *Quail Completions*>)
(buffer-list #<buffer *scratch*> #<buffer *Messages*> #<buffer *Minibuf-1*> #<buffer init.org> #<buffer *Org Agenda*> #<buffer *Group*> #<buffer *eshell*>)
(set-info :source | A cohort scheduling example. |)
(set-info :smt-lib-version 2.0)
(set-option :produce-models true)
;;; The budget indicates how large any one group can be
(declare-fun budget () Int)
(assert (= budget 20))
;;; The total number of groups
(declare-fun groups () Int)

Given a function f : a → b → c, if someone presents me with a term of the following type:

∀ (x : a) (y : c), ∃ (w : b), f x w = y

then I know y is a result of f x apply to some w.

However, if w must remain unknown, there is a problem with this term: it is only acceptable in the form of a constructive witness, which means I could inspect the existential to learn w.

Local asset trading

Lockup funds into an L2 prior to some event where the standard forms of payment may not be readily accessible, like on an airplane or a cruise ship. Customers are able to transact and purchase while on the trip, and then the activity is settled back to the L1 and the standard monetary exchanges after the conclusion of the trip.

This indicates a type of scenario allows for local economies that integrate back into the global economy after a period of time when it may not be possible to perform activity directly within the global economy: like during a trip, or during a crisis.

Another example of where this would become quite necessary is if Mars were colonized. In that case, you would want two global economies for each planet, but they should be able to reflect transactions back and forth with complete security.

Certification

(defun gnus-harvest-org-contacts-complete-name (string)
"Complete text at START with a user name and email."
(let* ((completion-ignore-case org-contacts-completion-ignore-case)
(completion-list
(cl-loop for contact in (org-contacts-filter)
;; The contact name is always the car of the assoc-list
;; returned by `org-contacts-filter'.
for contact-name = (car contact)
;; Build the list of the email addresses which has
---- MODULE SynchronousL2 ----
EXTENDS TLC, Naturals, Integers, Sequences, FiniteSets
CONSTANT Supply
(* --termination --fair algorithm SynchronousL2 {
variables
Accounts = [ Alice |-> Supply \div 2
(module coin GOVERNANCE
@doc "'coin' represents the Kadena Coin Contract. This contract provides both the \
\buy/redeem gas support in the form of 'fund-tx', as well as transfer, \
\credit, debit, coinbase, account creation and query, as well as SPV burn \
\create. To access the coin contract, you may use its fully-qualified name, \
\or issue the '(use coin)' command in the body of a module declaration."
@model
[ (defproperty conserves-mass
1 (map (insert-nft-offer) items)
1 (map (pool.slash) endorsed) ]
1 (map (format-item) items)
1 (+ subs (get-wizard-fields-for-ids (map (get-only-id) subs)))
1 (drain-result (map (drain-account) accounts))
1 (map (init-init) old-nft-ids)
1 (sweep-result (map (sweep-one) pairs))
1 ; (map (select-valid-offers-for-id) owned-miners)
1 (length-list (map (length) matrix)) ; get length of every row
1 (map (get-gallina-details-obj) x))
Athena ~ $ for i in /cores/core.* ; do lldb -c "$i" --batch -o 'thread backtrace' -o 'quit' ; done
(lldb) target create --core "/cores/core.33041"
Core file '/cores/core.33041' (arm64) was loaded.
(lldb) thread backtrace
* thread #33, stop reason = ESR_EC_DABORT_EL0 (fault address: 0x22a)
* frame #0: 0x0000000105bf0c28 chainweb-node`___lldb_unnamed_symbol1077568 + 16
(lldb) quit
(lldb) target create --core "/cores/core.333"
Core file '/cores/core.333' (arm64) was loaded.
(lldb) thread backtrace