nbun

{-# OPTIONS_GHC
    -ddump-simpl
    -dsuppress-idinfo
    -dsuppress-coercions
    -dsuppress-type-applications
    -dsuppress-uniques
    -dsuppress-module-prefixes
#-}

import           Debug.Trace

nbun

{-# OPTIONS_GHC
    -ddump-simpl
    -dsuppress-idinfo
    -dsuppress-coercions
    -dsuppress-type-applications
    -dsuppress-uniques
    -dsuppress-module-prefixes
#-}

import           Debug.Trace

nbun

{-# OPTIONS_GHC
    -ddump-simpl
    -dsuppress-idinfo
    -dsuppress-coercions
    -dsuppress-type-applications
    -dsuppress-uniques
    -dsuppress-module-prefixes
#-}

import           Control.Monad

nbun

{-# OPTIONS_GHC
    -ddump-simpl
    -dsuppress-idinfo
    -dsuppress-coercions
    -dsuppress-type-applications
    -dsuppress-uniques
    -dsuppress-module-prefixes
#-}

import           Debug.Trace

nbun

package nfc;

import java.awt.MouseInfo;
import java.awt.Robot;
import java.awt.event.KeyEvent;
import java.util.List;

import javax.smartcardio.*;

public class SmartCardReader {

nbun

Class HContainer : Type :=
  {
    Shape : Type;
    Pos : Shape -> Type;
    Ctx : forall s : Shape, Pos s -> Type -> Type;
  }.

Inductive Ext (C : HContainer) (F : Type -> Type) A :=
ext : forall s, (forall p : Pos s, F (Ctx s p A)) -> Ext C F A.

nbun

Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Program.Equality.

Inductive Ext Shape (Pos : Shape -> Type -> Type -> Type) (F : Type -> Type) A :=
  ext : forall s, (forall X, Pos s A X -> F X) -> Ext Shape Pos F A.

Arguments ext {_} {_} {_} {_} s pf.

Set Implicit Arguments.

nbun

{-# LANGUAGE DeriveFunctor         #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms       #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}