Crunchez vos adresses URL
|
Calculez la conso électrique de votre PC
|
Hébergez vos photos
Page 29 sur 29 PremièrePremière ... 19212223242526272829
Affichage des résultats 841 à 845 sur 845
  1. #841
    Oula, quand je faisais du Coq, c'était un petit peu plus simple

  2. #842
    Y'a pas une version GPU ?
    Sombrero d'or since 2015/12/03
    Citation Envoyé par Darkath Voir le message
    Mais enfin c'est toi l'expert, trouve des solutions bordel.

  3. #843
    Oh si.
    Plutôt qu'une preuve, on fait voter tous les coeurs et on compte les résultats.

    Je -> []

  4. #844
    Une chose est sûre, les GPUs, si on les faisait voter, ne voteraient pas pour les écolos
    Sombrero d'or since 2015/12/03
    Citation Envoyé par Darkath Voir le message
    Mais enfin c'est toi l'expert, trouve des solutions bordel.

  5. #845
    Citation Envoyé par taronyu26 Voir le message
    Y'a pas une version GPU ?
    Pas que je sache, mais techniquement, je pense que ça pourrait. Il y a quelques papiers sur la parallélisation du moteur de typage de Haskell, donc pourquoi pas celui de Coq. Il y a aussi des tactiques brute-force dont la recherche pourrait surement être parallélisée.

    Pour rappel, voici les principales tactiques de Coq, et leur traduction en maths :

    Code:
    trivial.
    Trivial.

    Code:
    simpl.
    Par un calcul évident.

    Code:
    omega.
    Preuve calculatoire simple, omise.

    Code:
    auto.
    Démonstration laissée en exercice.

    Code:
    auto with *.
    Par application d'un théorème de Gauss.

    Code:
    intuition.
    Voir preuve dans la marge.

Règles de messages

  • Vous ne pouvez pas créer de nouvelles discussions
  • Vous ne pouvez pas envoyer des réponses
  • Vous ne pouvez pas envoyer des pièces jointes
  • Vous ne pouvez pas modifier vos messages
  •