Commits

Commit history

1. Commits on Sep 8, 2026

   • copilot-theorem: Remove unnecessary extension. Refs #733.

     Show description for 0f1ebfc
     ivanperez-keera

     committed
     0f1ebfcView commit details

     Copy full SHA for 0f1ebfc

     View code at this pointBrowse repository at this point
2. Commits on Jul 8, 2026

   • copilot-theorem: Extend range of versions of Kind2. Refs #734.

     Show description for 5de4a7b
     

     chathhorn-galois

     authored and

     ivanperez-keera

     committed
     5de4a7bView commit details

     Copy full SHA for 5de4a7b

     View code at this pointBrowse repository at this point
3. Commits on Apr 3, 2026

   • copilot-theorem: Handle special Float values correctly for counterexamples. Refs #697.

     Show description for caafd77
     

     tkann-galois

     and

     RyanGlScott

     committed
     caafd77View commit details

     Copy full SHA for caafd77

     View code at this pointBrowse repository at this point
4. Commits on Sep 7, 2025

   • copilot-theorem: Remove unused function Copilot.Theorem.Misc.SExpr.parseSExpr. Refs #661.

     Show description for 70544fb
     ivanperez-keera

     committed
     70544fbView commit details

     Copy full SHA for 70544fb

     View code at this pointBrowse repository at this point
5. Commits on Jul 2, 2025

   • copilot-theorem: Remove 'LambdaCase' unused pragma from 'SMTIO.hs'. Refs #613.

     Show description for 2d101a7
     

     carte731

     authored and

     carte731

     committed
     2d101a7View commit details

     Copy full SHA for 2d101a7

     View code at this pointBrowse repository at this point

   • copilot-theorem: Remove 'LambdaCase' unused pragma from 'Prover.hs'. Refs #613.

     Show description for bbb90b6
     

     carte731

     authored and

     carte731

     committed
     bbb90b6View commit details

     Copy full SHA for bbb90b6

     View code at this pointBrowse repository at this point

   • copilot-theorem: Remove 'TupleSections' unused pragma from 'what4.hs'. Refs #613.

     Show description for 3088023
     

     carte731

     authored and

     carte731

     committed
     3088023View commit details

     Copy full SHA for 3088023

     View code at this pointBrowse repository at this point

   • copilot-theorem: Remove 'TemplateHaskell' unused pragma from 'what4.hs'. Refs #613.

     Show description for 61fa0b4
     

     carte731

     authored and

     carte731

     committed
     61fa0b4View commit details

     Copy full SHA for 61fa0b4

     View code at this pointBrowse repository at this point

   • copilot-theorem: Remove 'StandaloneDeriving' unused pragma from 'what4.hs'. Refs #613.

     Show description for 4f5f09a
     

     carte731

     authored and

     carte731

     committed
     4f5f09aView commit details

     Copy full SHA for 4f5f09a

     View code at this pointBrowse repository at this point

   • copilot-theorem: Remove 'MultiWayIf' unused pragma from 'what4.hs'. Refs #613.

     Show description for ad38ba4
     

     carte731

     authored and

     carte731

     committed
     ad38ba4View commit details

     Copy full SHA for ad38ba4

     View code at this pointBrowse repository at this point

   • copilot-theorem: Remove 'GeneralizedNewtypeDeriving' unused pragma from 'what4.hs'. Refs #613.

     Show description for 282a78f
     

     carte731

     authored and

     carte731

     committed
     282a78fView commit details

     Copy full SHA for 282a78f

     View code at this pointBrowse repository at this point
6. 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
7. 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
8. 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
9. 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
10. 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
11. 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
12. 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
13. 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
14. 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
15. 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
16. 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
17. 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
18. 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
19. 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
20. 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
21. 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