rzrn

{-# OPTIONS --cubical #-}
module Experiments where

open import Agda.Builtin.Cubical.Path public
open import Agda.Builtin.Cubical.Sub public renaming (primSubOut to ouc)
open import Agda.Primitive.Cubical public
  renaming ( primIMin       to _∧_  -- I → I → I
           ; primIMax       to _∨_  -- I → I → I
           ; primINeg       to -_   -- I → I
           ; isOneEmpty     to empty

rzrn

type expr =
  | EVar of string
  | EApp of expr * expr
  | EPi of string * expr * expr
  | ESig of string * expr * expr
  | ELam of string * expr * expr
  | EPair of expr * expr
  | EFst of expr
  | ESnd of expr
  | ESet of int

rzrn

@.fizz = private unnamed_addr constant [6 x i8] c"fizz \00"
@.buzz = private unnamed_addr constant [6 x i8] c"buzz \00"
@.integer = private unnamed_addr constant [4 x i8] c"%d \00"

@nl = private unnamed_addr constant [2 x i8] c"\0A\00"

declare i32 @printf(i8* noalias nocapture, ...) nounwind

define void @fizzbuzz(i32 %n) {
    %fizz = getelementptr [6 x i8], [6 x i8]* @.fizz, i64 0, i64 0

rzrn

from random import randint

print("Введите число коробок: ", end='')
N = int(input())

# Ставит мышь в случайное место
def initmouse():
    # Да-да, глобальная переменная, фу‐фу
    global mouse
    mouse = randint(1, N)

rzrn

from random import choice
from sys import argv

alphabet = {
    'А': list("丹升什闩"), 'Б': list("石右五"),
    'В': list("归乃巧日扫丑"), 'Г': list("厂广"),
    'Д': list("亼 囗"), 'Е': list("巨乞仨巳它正臣亖"),
    'Ё': ["庄"], 'Ж': list("水卌兴川氽米"), 'З': list("乡弓了"),
    'И': ["仈"], 'Й': list("订计认"), 'К': list("片长"), 'Л': list("几人穴入"),
    'М': list("从册爪"), 'Н': list("廾卄"), 'О': ["口"],

rzrn

(macros
  { :circuit
    (fn [...]
      (local k (length [...]))
      (if (= (% k 5) 0)
        (do
          (local j (/ k 5)) (local res { })
          (for [i 1 j]
            (local n (* i 5))
            (tset res i

rzrn

@[derive decidable_eq] structure dim := (L M T I Θ N J : int)

def dim.one := dim.mk 0 0 0 0 0 0 0
def L := { dim.one with L := 1 }
def M := { dim.one with M := 1 }
def T := { dim.one with T := 1 }
def I := { dim.one with I := 1 }
def Θ := { dim.one with Θ := 1 }
def N := { dim.one with N := 1 }
def J := { dim.one with J := 1 }

rzrn

import data.buffer.parser
open parser

inductive res
| str : string → res
| int : int → res
| ch : char → res

instance res_repr : has_repr res :=
⟨λ x, match x with

rzrn

#! /usr/bin/env pwsh-preview

herbstclient emit_hook reload
herbstclient keyunbind --all
herbstclient mouseunbind --all

$Mod = 'Mod1'
$terminal = 'uxterm'
$resizestep = 0.05
$wallpaper = '~/Pictures/background.png'