Iainmon

import Init.Data.ToString.Basic


namespace TreePatterns

variable {γ : Type} [BEq γ] [ToString γ]


abbrev Name := String

Iainmon

import Init.Data.ToString.Basic


namespace TreePatterns

variable {γ : Type} [BEq γ] [ToString γ]

#check 1

abbrev Name := String

Iainmon

from pycparser import c_parser, c_generator


# -----------------------------
# CFG data structures
# -----------------------------
class BasicBlock:
    def __init__(self, block_id):
        self.id = block_id
        self.stmts = []

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.