lynaghk

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;;  Solo freelancer's S-Corp tax optimization
;;
;;  Assumes an unmarried single-shareholder and tons of other stuff.
;;  I'm not a tax professional, no guarantees here, probably typos, etc. Come on!
;;  Run with https://github.com/Z3Prover/z3
;;
;;  See also my notes at https://kevinlynagh.com/financial-plan/

evancz

module Hints exposing (..)

import List
import Html exposing (..)
import Html.Attributes as A

{-----------------------------------------------------------

      SYNTAX HINTS (OCaml -> Elm)

mb64

(* Itty bitty SMT solver: DPLL(T) where T = equality *)
(*
# let x, y = 0, 1 (* integer variable IDs *) ;;
# let prob = SMT.new_problem 2 (* 2 for two variables *) ;;
# let b = SMT.new_bool prob;;  
# SMT.add_clause prob [b; SMT.eq prob x y];
  SMT.add_clause prob [SMT.not b];
  SMT.solve prob;;
- : SMT.response = SMT.SAT
# SMT.add_clause prob [SMT.not (SMT.eq prob x y)];

mb64

(* Typechecker for MLTT with a universe hierarchy *)
(* Build with: ocamlfind ocamlc -package angstrom,stdio -linkpkg mltt.ml -o mltt *)
type name = string

module AST = struct
  type tm =
    | Var of name
    | U of int
    | Pi of name * ty * ty
    | Annot of tm * ty

mb64

type name = string

module AST = struct
  type ty =
    | TFun of ty * ty
    | TNamed of string
    | TApp of ty * ty

  type exp =
    | Annot of exp * ty

isovector

{-# LANGUAGE DeriveFunctor          #-}
{-# LANGUAGE DeriveGeneric          #-}
{-# LANGUAGE DerivingStrategies     #-}
{-# LANGUAGE DerivingVia            #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE NoStarIsType           #-}
{-# LANGUAGE PatternSynonyms        #-}

AndrasKovacs

Require Import Coq.Unicode.Utf8.

(*
As far as I can tell, there is way more literature in Agda on datatype-generic
programming than in Coq. I think part of the reason is that the Agda literature
makes liberal use of induction-recursion and fancy termination/positivity
checking, to define fixpoints of functors. These features are not available in
Coq.

kkrypt0nn

A guide to ANSI on Discord

Discord is now slowly rolling out the ability to send colored messages within code blocks. It uses the ANSI color codes, so if you've tried to print colored text in your terminal or console with Python or other languages then it will be easy for you.

Quick Explanation

To be able to send a colored text, you need to use the ansi language for your code block and provide a prefix of this format before writing your text:

\u001b[{format};{color}m

\u001b is the unicode escape for ESCAPE/ESC, meant to be used in the source of your bot (see ). If you wish to send colored text without using your bot you need to copy the character from the website.

wenkokke

Tactics in Agda

This gist is my attempt to list all projects providing proof automation for Agda.

Glossary

When I say tactic, I mean something that uses Agda's reflection to provide a smooth user experience, such as the solveZ3 tactic from Schmitty:

_ : ∀ (x y : ℤ) → x ≤ y → y ≤ x → x ≡ y
_ = solveZ3

TOTBWF

{-# OPTIONS --allow-exec #-}

-- Embed a file as a string inside of an agda program.
-- To use this, make sure to add '/bin/cat' to '~/.agda/executables'

module Static where

open import Function

open import Data.Unit