Iainmon

import Init.Core
import Init.Prelude
import Mathlib.Algebra.Group.Defs
import Mathlib.Tactic


namespace Q10

class Req (α : Type) extends Semigroup α where
  eᵣ : α

Iainmon

Section S.

Context {A B : Set}.

Context (rel : A -> B -> Prop).


Definition determinism : Type 
  := forall (a : A) (b1 b2 : B), rel a b1 -> rel a b2 -> b1 = b2.

Iainmon

module Prim


import Data.Vect
import Data.Fin
-- import Data.Nat
-- import Data.List
-- %hide Prelude.cong

Iainmon

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] _ _.

Iainmon

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.

Iainmon

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 :=

Iainmon

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.

Iainmon

module Ficu where

import Text.Parsec
    ( anyChar,
      char,
      noneOf,
      oneOf,
      between,
      choice,
      many1,

Iainmon

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];
    }
}

Iainmon

INCLUDE Irvine32.inc

; #define MAX_ITER 45
; int main() {
;     int n;
;     int m;
;     int tmp;
;     int i;
;     i = 0;
;     n = 0;