-
Notifications
You must be signed in to change notification settings - Fork 1
/
nm_fun.v
20 lines (18 loc) · 915 Bytes
/
nm_fun.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
(**************************************************************)
(* Copyright Dominique Larchey-Wendling [*] *)
(* Jean-François Monin [+] *)
(* *)
(* [*] Affiliation LORIA -- CNRS *)
(* [+] Affiliation VERIMAG - Univ. Grenoble-Alpes *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(**************************************************************)
(** Swap Import and Export to exchange between
_acc: accessibility based domain predicate
_bar: custom inductive domain predicate
_mid: another approach by JFM
*)
Require Import nm_fun_acc.
Require Import nm_fun_mid.
Require Export nm_fun_bar.