search

CoqHott / coq-forcing

A plugin for Coq that implements the call-by-name forcing translation
12 stars 3 forks source link

Forcing translation of propositions #6

Open herbelin opened 3 years ago

herbelin commented 3 years ago

For the record, I found an issue with the forcing translation of Props:

From Forcing Require Import Forcing.
Axiom Obj : Type.
Axiom Hom : Obj -> Obj -> Type.
Notation "P ≤ Q" := (forall R, Hom Q R -> Hom P R) (at level 70).
Forcing Translate and using Obj Hom.
Forcing Translate iff using Obj Hom.
(* error: ...
has type
 "forall p : Obj,
  (forall p0 : Obj, p ≤ p0 -> forall p1 : Obj, p0 ≤ p1 -> Prop) ->
  (forall p0 : Obj, p ≤ p0 -> forall p1 : Obj, p0 ≤ p1 -> Prop) ->
  forall p0 : Obj, p ≤ p0 -> Type" while it is expected to have type
 "forall p : Obj,
  (forall p0 : Obj, p ≤ p0 -> forall p1 : Obj, p0 ≤ p1 -> Prop) ->
  (forall p0 : Obj, p ≤ p0 -> forall p1 : Obj, p0 ≤ p1 -> Prop) ->
  forall p0 : Obj, p ≤ p0 -> Prop".
*)

Apparently due to andᶠ declared in Type instead of Prop.