Commits

Commit history

1. Commits on Apr 17, 2025

   • copilot-theorem: Translate quantifiers correctly in Kind2 backend. Refs #594.

     Show description for a007efa
     RyanGlScott

     committed
     a007efaView commit details

     Copy full SHA for a007efa

     View code at this pointBrowse repository at this point

   • copilot-theorem: Add Props to specProps. Refs #594.

     Show description for 007e80a
     RyanGlScott

     committed
     007e80aView commit details

     Copy full SHA for 007e80a

     View code at this pointBrowse repository at this point
2. Commits on Mar 6, 2025

   • copilot-theorem: Reject existentially quantified propositions in What4 backend. Refs #254.

     Show description for d139242
     RyanGlScott

     committed
     d139242View commit details

     Copy full SHA for d139242

     View code at this pointBrowse repository at this point
3. Commits on Mar 5, 2025

   • copilot-theorem: Preserve proposition quantifiers. Refs Copilot-Language#254.

     Show description for bce4c10
     RyanGlScott

     committed
     bce4c10View commit details

     Copy full SHA for bce4c10

     View code at this pointBrowse repository at this point
4. Commits on Feb 27, 2025

   • copilot-theorem: Add Show and ShowF instances for counterexamples. Refs #589.

     Show description for 8d2a643
     RyanGlScott

     committed
     8d2a643View commit details

     Copy full SHA for 8d2a643

     View code at this pointBrowse repository at this point

   • copilot-theorem: Add function to produce counterexamples for invalid properties. Refs #589.

     Show description for c5ea1c0
     RyanGlScott

     committed
     c5ea1c0View commit details

     Copy full SHA for c5ea1c0

     View code at this pointBrowse repository at this point

   • copilot-theorem: Add XEmptyArray and XArray cases for valFromExpr. Refs #589.

     Show description for e23df09
     RyanGlScott

     committed
     e23df09View commit details

     Copy full SHA for e23df09

     View code at this pointBrowse repository at this point
5. Commits on Feb 24, 2025

   • copilot-theorem: Record Typed evidence in XEmptyArray and XArray. Refs #589.

     Show description for 86d7543
     RyanGlScott

     committed
     86d7543View commit details

     Copy full SHA for 86d7543

     View code at this pointBrowse repository at this point
6. Commits on Jan 29, 2025

   • copilot-theorem: Fix typo in documentation. Refs #587.

     Show description for 6bfb6a1
     ivanperez-keera

     committed
     6bfb6a1View commit details

     Copy full SHA for 6bfb6a1

     View code at this pointBrowse repository at this point
7. Commits on Dec 13, 2024

   • copilot-theorem: Remove uses of Copilot.Core.Expr.UExpr.uExprType,uExprExpr. Refs #565.

     Show description for 8852cc3
     kaBeech

     committed
     8852cc3View commit details

     Copy full SHA for 8852cc3

     View code at this pointBrowse repository at this point
8. Commits on Sep 6, 2024

   • copilot-theorem: Translate array updates to What4. Refs #36.

     Show description for a5d50f9
     

     RyanGlScott

     authored and

     ivanperez-keera

     committed
     a5d50f9View commit details

     Copy full SHA for a5d50f9

     View code at this pointBrowse repository at this point
9. Commits on Aug 30, 2024

   • copilot-theorem: Support translating `UpdateField` to what4. Refs #524.

     Show description for d939de5
     RyanGlScott

     committed
     d939de5View commit details

     Copy full SHA for d939de5

     View code at this pointBrowse repository at this point
10. Commits on May 5, 2024

    • copilot-theorem: Look for `falsifiable` (not `invalid`). Refs #495.

      Show description for 866a407
      RyanGlScott

      committed
      866a407View commit details

      Copy full SHA for 866a407

      View code at this pointBrowse repository at this point
11. Commits on Jan 8, 2024

    • copilot-theorem: Add explicit imports for Control.Monad. Refs #491.

      Show description for b826f42
      ivanperez-keera

      committed
      b826f42View commit details

      Copy full SHA for b826f42

      View code at this pointBrowse repository at this point

    • copilot-theorem: Mark module as trustworthy. Refs #491.

      Show description for 1c6e0c7
      ivanperez-keera

      committed
      1c6e0c7View commit details

      Copy full SHA for 1c6e0c7

      View code at this pointBrowse repository at this point
12. Commits on Nov 6, 2023

    • copilot-theorem: Update uses of arrayelems. Refs #457.

      Show description for 4f32459
      ivanperez-keera

      committed
      4f32459View commit details

      Copy full SHA for 4f32459

      View code at this pointBrowse repository at this point
13. Commits on Nov 3, 2022

    • copilot-theorem: Replace uses of Copilot.Core.Type.Equality. Refs #379.

      Show description for 670a6ca
      ivanperez-keera

      committed
      670a6caView commit details

      Copy full SHA for 670a6ca

      View code at this pointBrowse repository at this point
14. Commits on Oct 21, 2022

    • copilot-theorem: Use pretty-printer from copilot-prettyprinter. Refs #383.

      Show description for 38b28ed
      ivanperez-keera

      committed
      38b28edView commit details

      Copy full SHA for 38b28ed

      View code at this pointBrowse repository at this point
15. Commits on Oct 11, 2022

    • copilot-theorem: Add functionality for bisimulation proofs. Refs #363.

      Show description for 4ae3f24
      RyanGlScott

      committed
      4ae3f24View commit details

      Copy full SHA for 4ae3f24

      View code at this pointBrowse repository at this point
16. Commits on Apr 27, 2022

    • Style: make where keyword stand alone on one line. Refs #316.

      Show description for c1e0817
      ivanperez-keera

      committed
      c1e0817View commit details

      Copy full SHA for c1e0817

      View code at this pointBrowse repository at this point

    • Style: make where keyword stand alone on one line. Refs #316.

      Show description for 6c5e415
      ivanperez-keera

      committed
      6c5e415View commit details

      Copy full SHA for 6c5e415

      View code at this pointBrowse repository at this point

    • Style: make where keyword stand alone on one line. Refs #316.

      Show description for ba96bad
      ivanperez-keera

      committed
      ba96badView commit details

      Copy full SHA for ba96bad

      View code at this pointBrowse repository at this point

    • Style: make where keyword stand alone on one line. Refs #316.

      Show description for b027442
      ivanperez-keera

      committed
      b027442View commit details

      Copy full SHA for b027442

      View code at this pointBrowse repository at this point

    • Style: make where keyword stand alone on one line. Refs #316.

      Show description for 31b43b4
      ivanperez-keera

      committed
      31b43b4View commit details

      Copy full SHA for 31b43b4

      View code at this pointBrowse repository at this point

    • Style: make where keyword stand alone on one line. Refs #316.

      Show description for 0b765e8
      ivanperez-keera

      committed
      0b765e8View commit details

      Copy full SHA for 0b765e8

      View code at this pointBrowse repository at this point

    • Style: make where keyword stand alone on one line. Refs #316.

      Show description for d81cd3e
      ivanperez-keera

      committed
      d81cd3eView commit details

      Copy full SHA for d81cd3e

      View code at this pointBrowse repository at this point

    • Style: make where keyword stand alone on one line. Refs #316.

      Show description for 3560ee5
      ivanperez-keera

      committed
      3560ee5View commit details

      Copy full SHA for 3560ee5

      View code at this pointBrowse repository at this point

    • Style: make where keyword stand alone on one line. Refs #316.

      Show description for 71ba4f8
      ivanperez-keera

      committed
      71ba4f8View commit details

      Copy full SHA for 71ba4f8

      View code at this pointBrowse repository at this point

    • Style: make where keyword stand alone on one line. Refs #316.

      Show description for 7e00f71
      ivanperez-keera

      committed
      7e00f71View commit details

      Copy full SHA for 7e00f71

      View code at this pointBrowse repository at this point

    • Style: remove separating line in comment. Refs #316.

      Show description for f811c46
      ivanperez-keera

      committed
      f811c46View commit details

      Copy full SHA for f811c46

      View code at this pointBrowse repository at this point

    • Style: remove separating line in comment. Refs #316.

      Show description for febc19e
      ivanperez-keera

      committed
      febc19eView commit details

      Copy full SHA for febc19e

      View code at this pointBrowse repository at this point

    • Style: remove separating line in comment. Refs #316.

      Show description for 0aa48e4
      ivanperez-keera

      committed
      0aa48e4View commit details

      Copy full SHA for 0aa48e4

      View code at this pointBrowse repository at this point

    • Style: remove separating line in comment. Refs #316.

      Show description for a002d0c
      ivanperez-keera

      committed
      a002d0cView commit details

      Copy full SHA for a002d0c

      View code at this pointBrowse repository at this point

    • Style: remove separating line in comment. Refs #316.

      Show description for f372fa3
      ivanperez-keera

      committed
      f372fa3View commit details

      Copy full SHA for f372fa3

      View code at this pointBrowse repository at this point

    • Style: remove separating line in comment. Refs #316.

      Show description for b0327d7
      ivanperez-keera

      committed
      b0327d7View commit details

      Copy full SHA for b0327d7

      View code at this pointBrowse repository at this point