Navigation

Inscrivez-vous gratuitement
pour pouvoir participer, suivre les réponses en temps réel, voter pour les messages, poser vos propres questions et recevoir la newsletter

  1. #1
    Nouveau Candidat au Club
    Inscrit en
    janvier 2014
    Messages
    1
    Détails du profil
    Informations forums :
    Inscription : janvier 2014
    Messages : 1
    Points : 1
    Points
    1

    Par défaut [Coq] Travail sur les listes

    Bonjours à tous,

    Je suis débutant en Coq, et je voudrais écrire une fonction tous_satisfont qui construit la proposition : tous les éléments d’une liste satisfont une proposition donnée.

    Après avoir essayé pdt plusieurs heures, je crois que mon prob vient de la non compréhension de ce que représentent exactement les fonctions / propositions etc...

    Y aurait-il une âme charitable prête à me donner la correction de ma fonction que je puisse décortiquer tout seul ? Voilà ce que j'ai tapé...

    Fixpoint tous_satisfont (l : liste) (P : int -> Prop) : Prop :=
    match l with
    | [ ] => tous_satisfont [ ] P
    | x :: l' => P x
    end.

  2. #2
    Membre émérite
    Avatar de SpiceGuid
    Homme Profil pro
    Inscrit en
    juin 2007
    Messages
    1 692
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 692
    Points : 2 957
    Points
    2 957

    Par défaut

    Citation Envoyé par HeatBurns
    Je suis débutant en Coq
    Moi aussi.
    Ton véritable handicap c'est que tu es également débutant en programmation fonctionnelle.

    Code Coq : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    4
    5
    6
    7
    Require Import Coq.Lists.List.
    
    Fixpoint for_all (A:Type) l (p : A -> bool) :=
      match l with
      | nil => true
      | h :: t => if p h then for_all A t p else false  
      end.
    Du même auteur: le cours OCaml, le dernier article publié, le blog dvp et le jeu vidéo.
    Avant de poser une question je lis les règles du forum.

Discussions similaires

  1. Travail sur les listes
    Par Jiyuu dans le forum Tkinter
    Réponses: 6
    Dernier message: 08/04/2008, 21h53
  2. [MFC][Visual C++ 6]Travail sur les dates
    Par tus01 dans le forum MFC
    Réponses: 6
    Dernier message: 31/01/2006, 21h32
  3. GDI - Travail sur les pixels dans un DIB
    Par jiib dans le forum Windows
    Réponses: 3
    Dernier message: 12/12/2005, 13h17

Partager

Partager
  • Envoyer la discussion sur Viadeo
  • Envoyer la discussion sur Twitter
  • Envoyer la discussion sur Google
  • Envoyer la discussion sur Facebook
  • Envoyer la discussion sur Digg
  • Envoyer la discussion sur Delicious
  • Envoyer la discussion sur MySpace
  • Envoyer la discussion sur Yahoo