codyroux

Notation "P ≢ Q" := (~(P <-> Q))(at level 100).

Theorem no_middle : ~(exists P, (P ≢ True) /\ (P ≢ False)).
Proof.
  intro h.
  destruct h as [P [h1 h2]].
  apply h2.
  split; [ | intros h; contradiction].
  intros h3.
  apply h1; split; auto.

codyroux

Require Import Lia.

Section Iter_to_ind.

  Variable B : Prop.
  Variable F : Prop -> Prop.

  Hypothesis F_ext : forall P Q, (P <-> Q) -> (F P <-> F Q).
  
  Fixpoint iter_prop (n : nat) : Prop :=

codyroux

type term =
  | Var of int
  | Num of int
  | App of term * term
  | Lam of term
  | Plus of term * term
  | Ite of term * term * term

type input = { mutable pos : int; mutable str : string }

codyroux

#include <stdio.h>
#include <stdlib.h>

#define MEM_SIZE 1000000000 //10^9

struct mem_array {
  size_t buff_size;
  char * addr;
};

codyroux

mutual
inductive Subst : Type where
| ids : Subst
| tcons : Term → Subst → Subst
| shift : Subst
| comp : Subst → Subst → Subst
inductive Term : Type where
| var : Term
| lam : Term → Term

codyroux

module Map = Map.Make(String)

type ref_pointer = int
(* The type of values, that is the output of a terminating computation *)
type value = Int of int | Clos of env * term | Ref of ref_pointer
(* The type of programs *)
and term = Var of string
         | Let of string * term * term
         | Print of term
         | Lit of int