anlun

Require Import BinInt ZArith_dec Zorder.
Require Export Id.
Require Export State.
Require Export Expr.

From hahn Require Import HahnBase.

Definition eval_op (op : bop) (z1 z2 : Z) : option Z :=
  match op with
  | Add => Some (z1 + z2)%Z

anlun

use egg::*;

define_language! {
    enum RelLanguage {
        "top" = Top,
        "bot" = Bot,

        ";;" = Seq([Id; 2]),

        "+" = CT(Id),

anlun

#!/bin/bash
sed -i "s|\([a-zA-Z0-9\'\_]\+\)\.(\([a-zA-Z0-9\_\.\']\+\))\.(\([a-zA-Z0-9\_\.\']\+\))|(\3 (\2 \1))|g" src/*/*.v
sed -i "s|\([a-zA-Z0-9\'\_]\+\)\.(\([a-zA-Z0-9\_\.\']\+\))|(\2 \1)|g" src/*/*.v
sed -i "s|\(([a-zA-Z0-9\'\_\.\ ]\+)\)\.(\([a-zA-Z0-9\_\.\']\+\))|(\2 \1)|g" src/*/*.v

anlun

From hahn Require Import Hahn.
Require Import Lia.
Require Import Bool List.
Export ListNotations.
Require Import Arith Arith.EqNat.
Require Extraction.

Inductive is_smallest : nat -> list nat -> Prop :=
  smallest_unit : forall n, is_smallest n [n]
| smallest_head : forall n m tl, 

anlun

From hahn Require Import Hahn.
Require Import Omega.
Require Import Bool List.
Export ListNotations.
Require Import Arith Arith.EqNat.
Require Extraction.

Inductive is_smallest : nat -> list nat -> Prop :=
  smallest_unit : forall n, is_smallest n [n]
| smallest_head : forall n m tl, 

anlun

From hahn Require Import Hahn.
Require Import Omega.
Require Import Bool List.
Export ListNotations.
Require Import Arith Arith.EqNat.
Require Extraction.

Inductive is_smallest : nat -> list nat -> Prop :=
  smallest_unit : forall n, is_smallest n [n]
| smallest_head : forall n m tl, 

anlun

#lang racket
(require redex/reduction-semantics)
(require (for-syntax racket/match))

(define-language L
  (E ::= (list v ... E e ...) (car E) (cdr E) hole)
  (v ::= (list v ...) natural)
  (e ::= (list e ...) (car e) (cdr e) natural))

(define-syntax-rule (==> a b)

anlun

#lang at-exp racket
(require redex/reduction-semantics)
(require "../core/parser.rkt")

(define term_RCU
  @prog{ ;; Preparing visible state counters.
        cw_na    := 0;
        cr1_na   := 0;
        cr2_na   := 0;
        lhead_na := null;