Ailrun

((nil
  (eval progn
        (let
            ((base-path
              (locate-dominating-file default-directory ".dir-locals.el")))
          ;; Custom backup path
          ;; Or you can set `make-backup-files` to `nil`.
          (make-local-variable 'backup-directory-alist)
          (add-to-list 'backup-directory-alist
                       `(".*" \,

Ailrun

{-# START_FILE package.yaml #-}
spec-version:                       0.31.0
name:                               {{name}}
version:                            0.1.0.0
# synopsis:
# description:
category:                           {{category}}{{^category}}Language{{/category}}
homepage:                           https://github.com/{{github-username}}{{^github-username}}Ailrun{{/github-username}}/{{name}}#readme
bug-reports:                        https://github.com/{{github-username}}{{^github-username}}Ailrun{{/github-username}}/{{name}}/issues
author:                             {{author-name}}{{^author-name}}Junyoung/Clare Jang{{/author-name}}

Ailrun

#!/usr/bin/env zsh
# Ailrun ZSH Theme

local -r default_PS1='${_user_host}${_current_dir} $(git_prompt_info)
%{$fg[${_caret_color}]%}%(!.!.>)%{$resetcolor%} '
local -r default_PS2='%{$fg[${_caret_color}]%}%(!.!.>)...%{$reset_color%} '
local -r default_RPS1='$(_git_time_since_commit) $(git_prompt_status) ${_return_status}'

if [[ -z "${INSIDE_EMACS}" ]]; then
    PS1="${default_PS1}"

Ailrun

{
  allowUnfree = true;

  packageOverrides = pkgs: with pkgs; rec {
    nixFontsConf = stdenv.mkDerivation {
      name = "nix-fonts-conf";
      version = "0.0.1";

      src = makeFontsConf {
        fontDirectories = [

Ailrun

Require Import Program.Equality.
Require Import Relations.Relation_Operators.
Require Relations.Operators_Properties.
Require Import Vectors.Vector.

Import VectorDef.VectorNotations.

Module OP := Operators_Properties.

Definition binseq n := VectorDef.t bool n.

Ailrun

{-# OPTIONS --safe #-}

open import Data.Bool renaming (Bool to 𝔹)
import Data.Bool as 𝔹
import Data.Bool.Properties as 𝔹ₚ
open import Data.Nat
open import Data.Vec hiding (concat; map)
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties

Ailrun

import Data.Bits
import Data.Bool

digitData :: [Int]
digitData = [63198, 18724, 59342, 62414, 37850, 62366, 63378, 37454, 63454, 37854]

chunk :: Int -> [a] -> [[a]]
chunk _ [] = []
chunk n as = take n as : chunk n (drop n as)

Ailrun

(define-sort MultiSet (T) (Array T Int))

(declare-const squirrels (MultiSet Int))

(assert (= (select squirrels 2) (select squirrels 3) (select squirrels 5) (select squirrels 8) (select squirrels 22) 1))
(assert (= (select squirrels 9) (select squirrels 12) 2))
(assert (= (store (store (store (store (store (store (store squirrels 2 0) 3 0) 5 0) 8 0) 9 0) 12 0) 22 0) ((as const (MultiSet Int)) 0)))

(define-fun round-cond ((s (MultiSet Int))) Bool
            (and