jwiegley

Inductive natural : Type :=
  | zero
  | succ (n : natural).

Fixpoint add (x y : natural) : natural :=
  match x with
  | zero => y
  | succ n => succ (add n y)
  end.

jwiegley

(* A C-valued presheaf on some category U.
  C is often taken to be Sets. *)
Definition Presheaf (U C : Category) := U^op ⟶ C.

(* A coverage on a category C consists of a function assigning to each object
   U ∈ C a collection of families of morphisms { fᵢ : Uᵢ → U } (i∈I), called
   covering families, such that

   if { fᵢ : Uᵢ → U } (i∈I) is a covering family
   and g : V → U is a morphism,

jwiegley

(lldb) target create --core "/cores/core.25283"
Core file '/cores/core.25283' (arm64) was loaded.
(lldb) thread backtrace
* thread #53, stop reason = ESR_EC_DABORT_EL0 (fault address: 0x60a8)
  * frame #0: 0x0000000108fee5f4 chainweb-node`stg_ap_0_fast + 12
(lldb) quit

jwiegley

Host athena
  User bgamari
  Port 2202
  HostName newartisans.hopto.org

jwiegley

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

jwiegley

      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))

jwiegley

(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

jwiegley

---- MODULE SynchronousL2 ----

EXTENDS TLC, Naturals, Integers, Sequences, FiniteSets

CONSTANT Supply

(* --termination --fair algorithm SynchronousL2 {

variables
    Accounts    = [ Alice |-> Supply \div 2

jwiegley

(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

jwiegley

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