zoeyfyi

module Main (main) where

import Agda.Compiler.Backend (Backend (..), Backend' (..), Recompile (Recompile), callBackend, setTCLens)
import Agda.Compiler.Common (IsMain (..))
import Agda.Interaction.BasicOps (atTopLevel)
import Agda.Interaction.FindFile (SourceFile (..))
import Agda.Interaction.Imports (CheckResult (..), Mode (..), parseSource, typeCheckMain)
import Agda.Interaction.Options qualified as A (defaultOptions)
import Agda.Syntax.Abstract.Name qualified as A (ModuleName, QName (..))
import Agda.Syntax.Internal qualified as A (Name (..))

zoeyfyi

lemma foobafafgw:
  assumes "∀ x. p x x"
      and "⋀ x y. (x, y) ∈ r ⟹ p x y"
      and "⋀ x y z. p x y ⟹ p y z ⟹ p x z"
    shows "(a, b) ∈ r⇧* ⟹ p a b"
proof (induct rule: rtrancl_induct)
  case base
  then show ?case
    using assms(1) by blast
next

zoeyfyi

/**
	{
		"api":1,
		"name":"Format jsonc",
		"description":"Cleans and format jsonc documents.",
		"author":"Ben",
		"icon":"broom",
		"tags":"json,prettify,clean,indent"
	}
**/

zoeyfyi

Require Import Coq.Classes.SetoidClass.

Program Instance Iff1Setoid{A:Type} : Setoid (A->Prop) := {|
  equiv := fun P Q => forall x, P x <-> Q x
|}.
Next Obligation.
  split.
  - intros P x; reflexivity.
  - intros P Q H x; symmetry; exact (H x).
  - intros P Q R H0 H1 x; transitivity (Q x); [exact (H0 x)|exact (H1 x)].

zoeyfyi

import sys
from copy import copy

n = 5
moves = [(1, 2), (1, -2), (-1, 2), (-1, -2), (2, 1), (2, -1), (-2, 1), (-2, -1)]

def intersect(p1, p2, p3, p4):
    # Going back on self
    if p1 == p4 and p2 == p3:
        return True

zoeyfyi

import re

def get_imports(source):
    imports = []
    i = 0
    while i < len(source)-1:
        print i
        # Find the next import
        i = source.find("#import", i, len(source))
        if i == -1:

zoeyfyi

import os

from pdfminer.pdfinterp import PDFResourceManager, PDFPageInterpreter
from pdfminer.converter import TextConverter
from pdfminer.layout import LAParams, LTRect, LTLine, LTTextBoxHorizontal
from pdfminer.pdfpage import PDFPage
from cStringIO import StringIO
from pdfminer.converter import PDFPageAggregator

from wand.image import Image

zoeyfyi

#include <llvm-c/Core.h>
#include <llvm-c/ExecutionEngine.h>
#include <llvm-c/Target.h>
#include <llvm-c/Analysis.h>
#include <llvm-c/BitWriter.h>

#define TEST_TYPE(name, src, expectedType) TEST(IrgenTest, name){       \
    Parser *parser = NewParser((char *)src, Lex((char *)src));          \
    Exp *e = ParseType(parser);                                         \
    Irgen *irgen = NewIrgen();                                          \

zoeyfyi

year = 2017
rpi = 0.02
inflation = 0.027778
maintance = 8570
start_fee = 9250

def loan(target, maint=maintance):
  return (start_fee * (1 + inflation) ** (target - year)) + maint