DmxLarchey

let is_fact n =
  let rec loop i n =
    let (q,r) = (n / i, n mod i)
    in not (r <> 0) && (q = 1 || loop (1+i) q)
  in 0 < n && loop 1 n;;

DmxLarchey

Require Import Relations.

Section Acc_clos_trans.

  Variables (X : Type) (R : X -> X -> Prop).

  Hint Constructors clos_trans : core.
  Hint Resolve Acc_inv : core.

  Lemma Acc_clos_trans x : Acc R x -> Acc (clos_trans _ R) x.

DmxLarchey

Require Import Arith Lia List Permutation.

Import ListNotations.

Set Implicit Arguments.

#[local] Notation "x ~p y" := (Permutation x y) (at level 70, no associativity, format "x  ~p  y").

Create HintDb perm_db.

DmxLarchey

Section Fin. 

  Inductive Fin : nat -> Type :=
  | Fz {n : nat} : Fin (S n)
  | Fs {n : nat} : Fin n -> Fin (S n).

  Inductive Fin_shape_O : Fin 0 -> Type := .

  Inductive Fin_shape_S {n} : Fin (S n) -> Type :=
    | Fin_shape_S_fst : Fin_shape_S Fz

DmxLarchey

# card is inserted

2015-04-09 23:41:49 scdaemon[27444] updating slot 0 status: 0x0007->0x0000 (11->12)
2015-04-09 23:41:49 scdaemon[27444] sending signal 12 to client 27442
2015-04-09 23:42:00 scdaemon[27444] updating slot 0 status: 0x0000->0x0007 (12->13)
2015-04-09 23:42:00 scdaemon[27444] sending signal 12 to client 27442

# card is read by gpg

2015-04-09 23:42:18 scdaemon[27444] DBG: send apdu: c=00 i=A4 p1=00 p2=0C lc=2 le=-1 em=0