This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Prim | |
import Data.Vect | |
import Data.Fin | |
-- import Data.Nat | |
-- import Data.List | |
-- %hide Prelude.cong |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import Coq.Init.Nat. | |
Inductive bit : Set := I | O. | |
Inductive bits : nat -> Set := | |
| bnil : bits 0 | |
| bcons : forall (n : nat), bit -> bits n -> bits (S n). | |
Arguments bcons [n] _ _. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import Unicode.Utf8. | |
Require Import Psatz. | |
Require Import Coq.Arith.Arith. | |
Require Import Coq.Init.Nat. (* needed? it seems no, with next line. *) | |
Import Nat. | |
Open Scope nat_scope. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Ltac save h1 h2 := | |
(*pose proof h1 as h2*) | |
let t := type of h1 in | |
assert (h2 : t) by (exact h1). | |
Tactic Notation "save" constr(h1) "as" ident(h2) := | |
save h1 h2. | |
(* Ltac replace_equivalent a b p := |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Lemma my_eq_sym: forall a b : Set, a = b -> b = a. | |
Proof. | |
intros a b. | |
intros H. | |
rewrite -> H || rewrite <- H. | |
reflexivity. | |
Qed. | |
Ltac inv H := inversion H; clear H; try subst. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Ficu where | |
import Text.Parsec | |
( anyChar, | |
char, | |
noneOf, | |
oneOf, | |
between, | |
choice, | |
many1, |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
proc convShape() {} | |
iter regions(dom: domain(2,int), k: int, stride: int) { | |
const (h,w) = convShape(dom.shape,k,stride,padding=0); | |
for (i,j) in {0..#h,0..#w} { | |
yield dom[i * k * stride..#k,j * k * stride..#k]; | |
} | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
INCLUDE Irvine32.inc | |
; #define MAX_ITER 45 | |
; int main() { | |
; int n; | |
; int m; | |
; int tmp; | |
; int i; | |
; i = 0; | |
; n = 0; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import Control.Applicative ( Alternative(empty, (<|>)) ) | |
newtype Branch s a = Branch (s -> [(a,s)]) | |
branch :: (s -> [(a,s)]) -> Branch s a | |
branch = Branch | |
run :: Branch s a -> (s -> [(a,s)]) | |
run (Branch f) = f |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
const float rt = sqrt(2.); | |
float anim(float speed) { | |
return (.5*sin(iTime * speed)) + 0.5; | |
} | |
const vec3 paint = vec3(0.17, 0.55, 0.70); | |
void mainImage( out vec4 fragColor, in vec2 fragCoord ) |
NewerOlder