ghost-not-in-the-shell

open Core
open Async

let add_all file =
  Reader.file_contents file >>= fun contents ->
  let ls  = String.split_lines contents in
  let ss  = String.split_on_chars (String.concat ls) ~on:[','] in
  let ns  = List.map ss ~f:Int.of_string in
  let sum = List.fold_left ns ~init:0 ~f:(+) in
  printf "%d\n" sum;

ghost-not-in-the-shell

open Core
open Async

let parse contents = String.split_lines contents
                  |> String.concat
                  |> String.split_on_chars ~on:[',']
                  |> List.map ~f:Int.of_string

let read_then_sort fs =
  let ds = List.map ~f:Reader.file_contents fs

ghost-not-in-the-shell

{-# OPTIONS --without-K #-}
open import Data.Empty
open import Data.Sum
open import Function
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

_∙_ = trans

∙-unitʳ : ∀ {A : Set} {x y : A} (p : x ≡ y) → p ∙ refl ≡ p

ghost-not-in-the-shell

{-# OPTIONS --cubical #-}
open import Cubical.Core.Everything

refl₍_₎ : {A : Set} (x : A) → x ≡ x
refl₍ x ₎ = λ i → x

refl : {A : Set} {x : A} → x ≡ x
refl = refl₍ _ ₎

sym : {A : Set} {x y : A} → x ≡ y → y ≡ x

ghost-not-in-the-shell

{-# OPTIONS --cubical #-}
open import Cubical.Core.Everything hiding (_,_)

data Ty : Set where
  ι   : Ty
  _⇒_ : Ty → Ty → Ty

data Con : Set where
  ·   : Con
  _,_ : Con → Ty → Con

ghost-not-in-the-shell

{-# OPTIONS --cubical #-}
open import Cubical.Core.Everything hiding (_,_)

data Ty : Set where
  ι   : Ty
  _⇒_ : Ty → Ty → Ty

data Con : Set where
  ·   : Con
  _,_ : Con → Ty → Con

ghost-not-in-the-shell

{-# OPTIONS --cubical #-}
module Term where
open import Cubical.Core.Everything hiding (_,_)

data Ty : Set where
  ι   : Ty
  _⇒_ : Ty → Ty → Ty

infixl 5 _,_
data Con : Set where

ghost-not-in-the-shell

------------------------------------------------------------------------

An execution plan has been generated and is shown below.
Resource actions are indicated with the following symbols:
  ~ update in-place

Terraform will perform the following actions:

  # module.buildkite-east1-compute.aws_iam_user_policy.buildkite_aws_policy will be updated in-place
  ~ resource "aws_iam_user_policy" "buildkite_aws_policy" {

ghost-not-in-the-shell

function is_synced {
  local sync_status=$(mina client status | grep "Sync status" | cut -d":" -f2)
  if [ $? -ne 0 ];
  then
    echo Fail to fetch sync status
    return 0
  fi
  if [ $sync_status != "Synced" ];
  then 
    echo Nodes not synced

ghost-not-in-the-shell

import requests
import json
import time

query = """query {
  pooledUserCommands {
    hash
  }
}"""