In reply to @varikvalefor:matrix.org

.i ku'i la .varik. cu jinvi le du'u la lunra cu fanva fu le mleca be fi le ka ce'u mapti le sidbo be la .varik.

.i ji'a la .varik. cu djica lo nu lo javni cu me'oi .precise. ja co'e

.i ku'i la .varik. cu jinvi le du'u la lunra cu fanva fu le mleca be fi le ka ce'u mapti le sidbo be la .varik.

.i mi jimpe .i ku'i mi pu kaidji lo po'o ka ce'u birti lo nu mi smujmi lo javni

In reply to @luna.nightfern:catgirl.cloud

.i ku'i la .varik. cu jinvi le du'u la lunra cu fanva fu le mleca be fi le ka ce'u mapti le sidbo be la .varik.

.i mi jimpe .i ku'i mi pu kaidji lo po'o ka ce'u birti lo nu mi smujmi lo javni

.i xu zo ce'u zmadu

ni'o cadga fa lo nu ma ji'a javni

I think the current rules are good, idk what else should be added.

(sorry im very slow with lojban so i replied with english because it is inconvenient to use a dictionary on a mobile device)

In reply to @varikvalefor:matrix.org
sent a file.

In reply to @luna.nightfern:catgirl.cloud
.i ta mo

vvx@nerva:~$ file /home/vvx/Downloads/CD2PART1.MOD 
/home/vvx/Downloads/CD2PART1.MOD: 8-channel Fasttracker module sound data Title: "The decalogue"

"Fun, baby..."

takePawn : (q : GameData)
         → (m : Fin $ length $ GameData.haters q)
         → (n : Fin $ length $ GameData.itemsInRoomOf q m)
         → Σ GameData $ λ q'
           → Σ ((_≡_ on length ∘ GameData.rooms) q q') $ λ r
           → Σ ((_≡_ on length ∘ GameData.haters) q q') $ λ x
           → let xen = GameData.haters in
             let room = Character.room in
             (Σ (Character $ GameData.rooms q') $ λ k
              → ((_≡_ ⍨)
                  (xen q')
                  (Data.List.map
                    (kumfybi'o q q' r)
                    (_++_
                      (toℕ m ↑ xen q)
                      (_∷_
                        (kumfybi'o q' q (sym r) k)
                        (ℕ.suc (toℕ m) ↓ xen q))))))
           × (Σ Room $ λ r'
              → let kit = toℕ $ room $ xen q ! m in
                (_≡_
                  (GameData.rooms q')
                  (_++_
                    (kit ↑ GameData.rooms q)
                    (r' ∷ ℕ.suc kit ↓ GameData.rooms q))))
           × let iofink = GameData.yourfloorisnowclean in
             (_≡_
               q'
               record q {
                 rooms = GameData.rooms q';
                 haters = GameData.haters q';
                 player' = mink (GameData.player' q) x;
                 yourfloorisnowclean = iofink q'})
           × (_≡_
               (GameData.inventOf q' $ mink m x)
               ((_∷_ ⍨)
                 (GameData.inventOf q m)
                 (GameData.itemsInRoomOf q m ! n)))

In reply to @varikvalefor:matrix.org

"Fun, baby..."

takePawn : (q : GameData)
         → (m : Fin $ length $ GameData.haters q)
         → (n : Fin $ length $ GameData.itemsInRoomOf q m)
         → Σ GameData $ λ q'
           → Σ ((_≡_ on length ∘ GameData.rooms) q q') $ λ r
           → Σ ((_≡_ on length ∘ GameData.haters) q q') $ λ x
           → let xen = GameData.haters in
             let room = Character.room in
             (Σ (Character $ GameData.rooms q') $ λ k
              → ((_≡_ ⍨)
                  (xen q')
                  (Data.List.map
                    (kumfybi'o q q' r)
                    (_++_
                      (toℕ m ↑ xen q)
                      (_∷_
                        (kumfybi'o q' q (sym r) k)
                        (ℕ.suc (toℕ m) ↓ xen q))))))
           × (Σ Room $ λ r'
              → let kit = toℕ $ room $ xen q ! m in
                (_≡_
                  (GameData.rooms q')
                  (_++_
                    (kit ↑ GameData.rooms q)
                    (r' ∷ ℕ.suc kit ↓ GameData.rooms q))))
           × let iofink = GameData.yourfloorisnowclean in
             (_≡_
               q'
               record q {
                 rooms = GameData.rooms q';
                 haters = GameData.haters q';
                 player' = mink (GameData.player' q) x;
                 yourfloorisnowclean = iofink q'})
           × (_≡_
               (GameData.inventOf q' $ mink m x)
               ((_∷_ ⍨)
                 (GameData.inventOf q m)
                 (GameData.itemsInRoomOf q m ! n)))

In reply to @luna.nightfern:catgirl.cloud
.i .u'u mi na jimpe tu'a la'o gy. APL .gy. .i ta srana ma

.i me'oi .Agda. co'e

https://github.com/varikvalefor/textadventuretest/tree/agda-take-fegli

In reply to @varikvalefor:matrix.org

.i me'oi .Agda. co'e

https://github.com/varikvalefor/textadventuretest/tree/agda-take-fegli

In reply to @varikvalefor:matrix.org
sent an image.