fetburner

Require Import Arith NArith.

Notation reg := {n : nat | n < 32}.
Notation reg_dec := eq_nat_dec.
Notation i_format := (reg * reg * N)%type.
Notation r_format := (reg * reg * reg)%type.

Inductive inst : Set :=
  | ILW : i_format -> inst
  | ISW : i_format -> inst

fetburner

type __ = Obj.t
let __ = let rec f _ = Obj.repr f in Obj.repr f

type bool =
| True
| False

(** val negb : bool -> bool **)

let negb = function

fetburner

_require "basis.smi"

type coq___ = unit
val app : 'a1 list -> 'a1 list -> 'a1 list

val compOpp : order -> order

datatype compareSpecT =
  CompEqT
| CompLtT

fetburner

Require Import Arith List Operators_Properties Relation_Definitions Relation_Operators.

(* 変数名の識別子 *)
Parameter id : Type.
Parameter id_dec : forall x y : id, {x = y} + {x <> y}.

(* λ項の定義 *)
Inductive lambda_term :=
  | LVar : id -> lambda_term
  | LAbs : id -> lambda_term -> lambda_term

fetburner

let filter_map f l = List.fold_right (fun x l ->
  match f x with 
  | None -> l
  | Some y -> y :: l) l []
let rec unfold_right f init =
  match f init with
  | None -> []
  | Some (x, next) -> x :: unfold_right f next

(** x^2 + y^2 = rとなる(x, y)のリストを返す *)

fetburner

module Id =
  struct
    type t = string 
  end

module Token = 
  struct
    type t = Id of Id.t | BinOp of Id.t * (t * t) option | EOI
  end

fetburner

Require Import Arith List Operators_Properties Relation_Definitions Relation_Operators.

(* 項 *)
Inductive term :=
  | TmTrue : term
  | TmFalse : term
  | TmIf : term -> term -> term -> term
  | TmZero : term
  | TmSucc : term -> term
  | TmPred : term -> term

fetburner

theory Scratch
imports Main
begin

fun sum :: "nat \<Rightarrow> nat" where
"sum 0 = 0" |
"sum (Suc n) = Suc n + sum n"

theorem sum_of_n [simp]: "sum n = n * (n + 1) div 2"
apply (induction n)

fetburner

theory Scratch
imports Main
begin

fun pls :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
"pls 0 n = n" |
"pls (Suc m) n = Suc (pls m n)"

theorem pls_0_r [simp] : "pls n 0 = n"
apply (induction n)

fetburner

Inductive nt :=
  | Z : nt
  | Suc : nt -> nt.

Definition pls n m :=
  nt_rect _
    m
    (fun _ IH => Suc IH) n.

Definition mul n m :=