This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{ | |
allowUnfree = true; | |
packageOverrides = pkgs: with pkgs; rec { | |
nixFontsConf = stdenv.mkDerivation { | |
name = "nix-fonts-conf"; | |
version = "0.0.1"; | |
src = makeFontsConf { | |
fontDirectories = [ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/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}" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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}} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
((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 | |
`(".*" \, |