samuelgruetter

Require Import List.
Import ListNotations.
Require Import ssreflect.
Lemma test1 :
  length ([1] ++ [2]) = 2 ->
  2 = 4.
Proof.
  intros HA.
  evar (N : nat).
  Unshelve.

samuelgruetter

Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.
Require Import Ltac2.Ltac2.


(**** Parsing quote-less identifiers into Gallina Strings ****)

(* Takes a list of powers instead of one power and dividing because
   Ltac2 does not have integer division: https://github.com/coq/coq/issues/13802 *)
Ltac2 rec int_to_bits_rec(powers: int list)(val: int) :=

samuelgruetter

Require Import Coq.Strings.String. Open Scope string_scope.

Inductive expr :=
| EVar(x: string)
| ELam(x: string)(body: expr)
| EApp(f: expr)(arg: expr).

Declare Custom Entry ident_string.
Notation "x" := x (in custom ident_string at level 0, x constr at level 0).

samuelgruetter

Definition decidable (P: Prop) := {P} + {~P}.
Definition eq_dec T := forall (x y:T), decidable (x=y).

Inductive spec_type: Set :=
| abruption
| additiveExpression
| argumentList
| arguments
| arrayAssignmentPattern
| arrayBindingPattern

samuelgruetter

class A {
    var n: nat
    ghost var Repr: set<object>
    predicate Valid()
        reads this, Repr
    {
        this in Repr &&
        n % 2 == 0
    }
    constructor()

samuelgruetter

import javax.swing.*;
import java.awt.*;
import java.util.LinkedList;

import static java.lang.Math.*;

class DiscreteCircle {
    private final double radius;
    private static final double DOES_NOT_MATTER = 0;
    private static final double BIG_ANGLE_DIFF = 7.777;