Require Import Arith. Require Import BinPos. Extraction "pplus.ml" Pplus. Definition pred (n:nat) : n<>0 -> nat := match n as x return (x <> 0 -> nat) with | 0 => fun h : 0 <> 0 => False_rec nat (h (refl_equal 0)) | S p => fun _ : S p <> 0 => p end. Extraction pred. Definition pred0 := pred 0. Recursive Extraction pred0. Definition pred1 := pred 1. Recursive Extraction pred0 pred1. Fixpoint nArrow n : Set := match n with | O => nat | S n => nat -> nArrow n end. Fixpoint nSum n : nArrow (S n) := match n return nArrow (S n) with | O => fun a => a | S m => fun a b => nSum m (a+b) end. Recursive Extraction nSum. Axiom a:nat. Definition p (n:nat) := n+a. Recursive Extraction p. Definition dp := fun (A B:Set)(x:A)(y:B)(f:forall C:Set, C->C) => (f A x, f B y). Recursive Extraction dp.