Bryan Gin-ge Chen bryangingechen

## CreatingExternalSagePackages.md

      
              1 file
            
          
              0 forks
            
          
              5 comments
            
          
              2 stars
            
          
                cswiercz
                / CreatingExternalSagePackages.md
            
            
              Last active
              June 7, 2018 00:34
            
              
                A guide to creating a Sage package outside of Sage itself.
              
          
(Work in progress. Please suggest improvements.)

Creating External Sage Packages


Pure Python Package
Using Cython
Running Tests
Current Examples

Sometimes you want to write code that uses Sage and make it available to the

  
## README.md

      
              2 files
            
          
              0 forks
            
          
              0 comments
            
          
              5 stars
            
          
                sxv
                / README.md
            
            
              Last active
              July 3, 2018 07:20
            
              
                Interactive SVG + Canvas Plot
              
          
    A D3 demonstration of SVG and Canvas intermingling. Blue circles are plotted in SVG, black circles in canvas. One force to rule them all. The plot is zoomable and pannable.
Inspired by M. Bostock's Canvas / SVG zoom comparison series and collision detection examples [1] [2] .

  
## index.html
<!--
  Source:  https://gist.github.com/erikvullings/41be28677574fd484b43e91413a7e45d
  Preview: https://bl.ocks.org/erikvullings/41be28677574fd484b43e91413a7e45d
-->
<!DOCTYPE html>

<head>
  <meta charset="utf-8">
  <script src="https://d3js.org/d3.v4.min.js"></script>
  <style>

## extends_product.lean
/- The goal of this file is to explain why it's important that using extends in
   command `class foo extends bar` creates a `foo.to_bar` function with an
   instance implicit parameter.

   We will define magmas with law denoted by ◆ and a commutative version.
   Then we want products of such things. The goal is to reuse the work on product
   magmas when defining product commutative magmas, and do so in a completely
   transparent way. -/

-- Defining magmas with some notation is already covered in TPIL

## showdown-leftpad.lean

import data.list.basic

section left_pad

variables {α : Type*}

open nat

lemma list.cons_repeat (c : α) :

## showdown-unique.lean
section unique

variables {α : Type*} [decidable_eq α]

def unique : list α → list α
 | [] := []
 | (x :: xs) :=
   if x ∈ xs
     then unique xs
     else x :: unique xs

## AscList.agda
-- Reversing an ascending list in Agda.
-- Challenge by @arntzenius: https://twitter.com/arntzenius/status/1034919539467677696
module AscList where

-- We'll go without libraries to make things clearer.

flip : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → (A → B → C) → B → A → C
flip f x y = f y x

-- Step one is to define ordered lists. We'll roughly follow Conor McBride's approach

## rev_asc_desc.v
Require Import Coq.Lists.List Coq.Relations.Relations Coq.Sorting.Sorted.
Require Import Coq.Program.Equality Psatz.

Lemma Sorted_iff_by_explicit_indices {A} {R: relation A} (l: list A):
  Sorted R l <-> forall n, (S n) < length l -> exists d,
    R (nth n l d) (nth (S n) l d).
Proof with (cbn in *; firstorder).
  split; induction l; intros.
  - unshelve esplit; contradict H0...
  - unshelve esplit; intuition; inversion H.

## eckmann_hilton.lean
-- Written by Johan Commelin; golfed by Kenny Lau

import tactic.interactive

universe u

namespace eckmann_hilton
variables (X : Type u)

local notation a `<`m`>` b := @has_mul.mul X m a b

## indep.lean
import data.finset
open nat finset

/-- `indep E` is the type of matroids (encoded as systems of independent sets) with ground set `E` :
`finset α` -/
structure indep (α : Type*) [decidable_eq α] :=
(indep : finset (finset α))
-- (I1)
(empty_mem_indep : ∅ ∈ indep)
-- (I2)
	<!--
	Source: https://gist.github.com/erikvullings/41be28677574fd484b43e91413a7e45d
	Preview: https://bl.ocks.org/erikvullings/41be28677574fd484b43e91413a7e45d
	-->
	<!DOCTYPE html>

	<head>
	<meta charset="utf-8">
	<script src="https://d3js.org/d3.v4.min.js"></script>
	<style>
	/- The goal of this file is to explain why it's important that using extends in
	command `class foo extends bar` creates a `foo.to_bar` function with an
	instance implicit parameter.

	We will define magmas with law denoted by ◆ and a commutative version.
	Then we want products of such things. The goal is to reuse the work on product
	magmas when defining product commutative magmas, and do so in a completely
	transparent way. -/

	-- Defining magmas with some notation is already covered in TPIL

	import data.list.basic

	section left_pad

	variables {α : Type*}

	open nat

	lemma list.cons_repeat (c : α) :
	section unique

	variables {α : Type*} [decidable_eq α]

	def unique : list α → list α
	\| [] := []
	\| (x :: xs) :=
	if x ∈ xs
	then unique xs
	else x :: unique xs
	-- Reversing an ascending list in Agda.
	-- Challenge by @arntzenius: https://twitter.com/arntzenius/status/1034919539467677696
	module AscList where

	-- We'll go without libraries to make things clearer.

	flip : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → (A → B → C) → B → A → C
	flip f x y = f y x

	-- Step one is to define ordered lists. We'll roughly follow Conor McBride's approach
	Require Import Coq.Lists.List Coq.Relations.Relations Coq.Sorting.Sorted.
	Require Import Coq.Program.Equality Psatz.

	Lemma Sorted_iff_by_explicit_indices {A} {R: relation A} (l: list A):
	Sorted R l <-> forall n, (S n) < length l -> exists d,
	R (nth n l d) (nth (S n) l d).
	Proof with (cbn in *; firstorder).
	split; induction l; intros.
	- unshelve esplit; contradict H0...
	- unshelve esplit; intuition; inversion H.
	-- Written by Johan Commelin; golfed by Kenny Lau

	import tactic.interactive

	universe u

	namespace eckmann_hilton
	variables (X : Type u)

	local notation a `<`m`>` b := @has_mul.mul X m a b
	import data.finset
	open nat finset

	/-- `indep E` is the type of matroids (encoded as systems of independent sets) with ground set `E` :
	`finset α` -/
	structure indep (α : Type*) [decidable_eq α] :=
	(indep : finset (finset α))
	-- (I1)
	(empty_mem_indep : ∅ ∈ indep)
	-- (I2)