Commit ad328bd5 authored by Martin Clochard's avatar Martin Clochard
Browse files

(coq) add WhyType instance for arrow

parent 032b546b
Require Export ZArith. Require Export ZArith.
Require Export Rbase. Require Export Rbase.
Require Import ClassicalEpsilon.
Class WhyType T := { Class WhyType T := {
why_inhabitant : T ; why_inhabitant : T ;
why_decidable_eq : forall x y : T, { x = y } + { x <> y } why_decidable_eq : forall x y : T, { x = y } + { x <> y }
...@@ -58,3 +60,12 @@ split. ...@@ -58,3 +60,12 @@ split.
exact false. exact false.
exact Bool.bool_dec. exact Bool.bool_dec.
Qed. Qed.
Global Instance func_WhyType : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, WhyType (a -> b).
Proof.
intros.
repeat split.
exact (fun _ => why_inhabitant).
intros x y.
apply excluded_middle_informative.
Qed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment