yforster

(** Implementation of the Cantor pairing and its inverse function *)

Require Import PeanoNat Lia.

(** Bijections between [nat * nat] and [nat] *)

(** Cantor pairing [to_nat] *)

Fixpoint to_nat' z :=
  match z with

yforster

#!/bin/sh

coqtop -R . ""

yforster

;;
;; mode for .pi files 
;;

(defvar proverif-pi-kw '("among" "and" "can" "choice" "clauses" "data" "elimtrue" "else" "equation" "event" "fail" "free" "fun" "if" "in" "let" "new" "noninterf" "not" "nounif" "otherwise" "out" "param" "phase" "putbegin" "pred" "private" "process" "query" "reduc" "suchthat" "then" "weaksecret" "where") "ProVerif keywords")

(defvar proverif-pi-builtin '("memberOptim" "decompData" "decompDataSelect" "block" "attacker" "mess" "ev" "evinj") "ProVerif builtins")

(defvar proverif-pi-kw-regexp (regexp-opt proverif-pi-kw 'words))
(defvar proverif-pi-builtin-regexp (regexp-opt proverif-pi-builtin 'words))