palmskog

fun  valid_derivation_deriv_premise_cake v2 = 
    (fn  v1 => List.member v1 v2);

   datatype fitch_prop =  Prop_cont
  |  Prop_imp (fitch_prop) (fitch_prop)
  |  Prop_or (fitch_prop) (fitch_prop)
  |  Prop_and (fitch_prop) (fitch_prop)
  |  Prop_neg (fitch_prop)
  |  Prop_p (char list);

palmskog

Require Import List.
Require Import Arith.
Require Import Wellfounded.
Require Import Relation_Definitions.
Require Import Relation_Operators.
Require Import Lia.
From Coq Require Export ssreflect.
Global Set SsrOldRewriteGoalsOrder.
Global Set Asymmetric Patterns.
Global Set Bullet Behavior "None".

palmskog

Require Import List.
Require Import Arith.
Require Import Wellfounded.
Require Import Relation_Definitions.
Require Import Relation_Operators.
Require Import Lia.
From Coq Require Export ssreflect.
Global Set SsrOldRewriteGoalsOrder.
Global Set Asymmetric Patterns.
Global Set Bullet Behavior "None".

palmskog

Require Import List.
Require Import Arith.
Require Import Wellfounded.
Require Import Relation_Definitions.
Require Import Relation_Operators.
Require Import Lia.
From Coq Require Export ssreflect.
Global Set SsrOldRewriteGoalsOrder.
Global Set Asymmetric Patterns.
Global Set Bullet Behavior "None".

palmskog

(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/

Copyright (C) 2011-2018 Sylvie Boldo
#<br />#
Copyright (C) 2011-2018 Guillaume Melquiond

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public

palmskog

-R src TLC

src/LibAxioms.v
src/LibContainerDemos.v
src/LibEnv.v
src/LibExec.v
src/LibFset.v
src/LibHeap.v
src/LibListExec.v
src/LibList.v

palmskog

-R src Flocq

src/Version.v
src/Core/Raux.v
src/Core/Zaux.v
src/Core/Defs.v
src/Core/Digits.v
src/Core/Float_prop.v
src/Core/FIX.v
src/Core/Generic_fmt.v

palmskog

Require Import List.
Import ListNotations.

Set Implicit Arguments.

Fixpoint fin (n : nat) : Type :=
  match n with
    | 0 => False
    | S n' => option (fin n')
  end.

palmskog

Require Import List.
Import ListNotations.

Set Implicit Arguments.

Fixpoint before {A: Type} (x : A) y l : Prop :=
  match l with
    | [] => False
    | a :: l' =>
      a = x \/

palmskog

Require Import List.
Import ListNotations.

Set Implicit Arguments.

Section assoc.
  Variable K V : Type.
  Variable K_eq_dec : forall k k' : K, {k = k'} + {k <> k'}.

  Fixpoint assoc (l : list (K * V)) (k : K) : option V :=