travail sur Peano Axioms en Agda et a frappé un peu d'un point d'achoppement

Question

PA6 : ∀{m n} -> m ≡ n -> n ≡ m 

est l'axiome que je suis en train de résoudre et de soutien, je l'ai essayé d'utiliser un cong (à partir de la bibliothèque de base), mais je suis d'avoir des ennuis avec la constructeur cong

PA6 = cong 

me fait nulle part, je sais cong je suis tenu de fournir une réfl pour l'égalité et un type, mais je ne suis pas sûr du type que je suis censé fournir. Des idées? C'est pour une petite tâche à l'université, donc je préfère que quelqu'un montre ce que j'ai manqué plutôt que d'écrire la réponse acutual, mais j'apprécierais n'importe quel degré de soutien.

Answer 1

par la nature du système que j'avais créé, je devais réaliser que j'avais deux équivalences et donc besoin d'utiliser la méthode d'équivalence réfl

Ainsi pour satisfaire ma agda signature de type accepté: PA6 refl = refl

espérons que cela aide

Answer 2

Votre PA6 dit que ≡ est symétrique.

Ceci peut être trouvé dans la bibliothèque standard à partir du module Relation.Binary.PropositionalEquality.

sym : ∀ {a} {A : Set a} {x y : A} → x ≡ y → y ≡ x 
sym refl = refl 

(Cette question est assez vieux, mais je poste au profit des futurs lecteurs qui tombent par hasard sur elle.)