Documentation

LeanPool.PureNock.Reference

Standard Nock reference evaluator #

Fuel-indexed Nat-level evalN for OP₀–OP₁₁ (main.tex:1054–1076; OP₁₁ extension).

source
def Nock.Noun.wut :
Noun → Noun

? (Algorithm:Noun_Operators, main.tex:1519–1523). type(n)=cell ↦ 0, else ↦ 1.

Equations
Instances For
    source
    def Nock.Noun.lus :
    Noun → Option Noun

    + (Algorithm:Noun_Operators, main.tex:1531–1535). atom ↦ (1+n) (paper mod p; Lean Nat successor); else ⊥.

    Equations
    Instances For
      source
      def Nock.Noun.tis (a b : Noun) :
      Noun

      = (Algorithm:Noun_Operators, main.tex:1525–1529). n₁=n₂ ↦ 0, else ↦ 1.

      Equations
      Instances For
        source
        @[irreducible]
        def Nock.Noun.slot :
        Nat → Noun → Option Noun

        / (Algorithm:Noun_Operators, main.tex:1537–1557). axis=0 ↦ ⊥; =1 ↦ n; =2 ↦ head(n); =3 ↦ tail(n); else b←axis mod 2, return /(2+b, /((axis−b)/2, n)).

        Equations
        Instances For
          source
          @[irreducible]
          def Nock.Noun.edit :
          Nat → Noun → Noun → Option Noun

          # (Algorithm:Noun_Operators, main.tex:1587–1607). axis=0 ↦ ⊥; =1 ↦ new; else b←axis mod 2, a←(axis−b)/2, edit head/tail of parent at a, recurse #(a, parent, old).

          Equations
          Instances For
            source
            def Nock.evalN :
            Nat → Noun → Noun → Option Noun

            *[subject formula], fuel-indexed. evalN 0 _ _ = none.

            Equations
            Instances For