andrejbauer

/*
  This program is an adaptation of the Mandelbrot program
  from the Programming Rosetta Stone, see
  http://rosettacode.org/wiki/Mandelbrot_set

  Compile the program with:

  gcc -o mandelbrot -O4 mandelbrot.c

  Usage:

andrejbauer

andrejbauer

# 
METHOD: TABLE
ENCODE: Unicode
PROMPT: LaTeX
VERSION: 1.0
DELIMITER: ,
VALIDINPUTKEY: ^,.?!:;"'/\()[]{}<>$%&@*01234567890123456789ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz
TERMINPUTKEY: 
BEGINCHARACTER
alpha	α

andrejbauer

open import Data.Nat
open import Data.Fin as Fin

module Primrec where

  -- The datatype of primitive recursive function
  data PR : ∀ (k : ℕ) → Set where
    pr-zero : PR 0 -- zero
    pr-succ : PR 1 -- successor
    pr-proj : ∀ {k} (i : Fin k) → PR k -- projection

andrejbauer

(* A proof that there is a least closure operator which forces a given
   predicate to be true. The construction can be found in, e.g.,
   Martin Hyland's “Effective topos” paper, Proposition 16.3. *)

(* A closure operator on [Prop] is an idempotent, monotone, inflationary enodmap.

   One often requires additionally that the operator preserves conjunctions,
   in which case these are also called j-operators and Lawvere-Tierney topologies.
   We eschew the condition to obtain a slighly more general result, but we
   also show that the closure operator of interst happens to preserve conjunctions.

andrejbauer

(* A formalization of a classical propositional calculus a la user4035,
   see https://proofassistants.stackexchange.com/q/4443/169 and
   https://proofassistants.stackexchange.com/q/4468/169 ,
   with the following modifications:

   1) We use a set of assumptions rather than a list of assumptions.
   2) We use derivation trees to represent proofs instead of lists of formulas.

   Proofs-as-lists are used in Hilbert-style systems, whereas
   derivation trees are more common in natural-deduction style rules.

andrejbauer

{- Here is a short demonstration on how to use Agda's solvers that automatically
   prove equations. It seems quite impossible to find complete worked examples
   of how Agda solvers are used.

   Thanks go to @anormalform who helped out with these on Twitter, see
   https://twitter.com/andrejbauer/status/1549693506922364929?s=20&t=7cb1TbB2cspIgktKXU8rng

   I welcome improvements and additions to this file.

   This file works with Agda 2.6.2.2 and standard-library-1.7.1

andrejbauer

-- A predicative version of Tarski's fixed-point theorem

open import Level
open import Data.Product

module Tarski where

  -- a complete preorder with carrier at level a, the preorder is at level b,
  -- and suprema indexed by sets from level c
  record CompletePreorder a b c : Setω where

andrejbauer

Experiments involving Miquel's theorem. Joint work with Finn Klein.

andrejbauer

#!/usr/local/bin/python3

# Compute algebraic numbers in the complex plane and draw a nice picture

import numpy
import sys
import argparse
import math
import cairo
import pickle