Code

Coq inhabited errors#1470

Code

Merged

mergify[bot] merged 11 commits intomasterGaloisInc/saw-script:masterfrom coq-inhabitedGaloisInc/saw-script:coq-inhabitedCopy head branch name to clipboardOct 12, 2021

+1,430-1,212

Commits

Commits on Oct 11, 2021

• Define a new Inhabited typeclass that restricts the types that

  Show description for c2eb434
  robdockins

  committed
  c2eb434

  Copy full SHA for c2eb434

• Introduce an annotation on sorts that classify types that are expected to be inhabited.

  Show description for 756cac4
  robdockins

  committed
  756cac4

  Copy full SHA for 756cac4

• Add support for translating the new isort inhabited sort

  Show description for 03c7344
  robdockins

  committed
  03c7344

  Copy full SHA for 03c7344

• Update the SAWCore prelude by inserting isort annotations where

  Show description for 39c3f8c
  robdockins

  committed
  39c3f8c

  Copy full SHA for 39c3f8c

• Add a new "injectCode" declaration to SAWCore.

  Show description for 48d4d8a
  robdockins

  committed
  48d4d8a

  Copy full SHA for 48d4d8a

• Update the Cryptol/SAWCore prelude to incorporate inhabitated annotations.

  robdockins

  committed
  a37e766

  Copy full SHA for a37e766

• Check in generated Coq files for the SAWCore and Cryptol preludes.

  robdockins

  committed
  f1dc215

  Copy full SHA for f1dc215

• Revert changes to the implicit argument of letRecM.

  Show description for 179acd5
  robdockins

  committed
  179acd5

  Copy full SHA for 179acd5

• Improved documentation for the SpecialTreatement module

  Show description for db984b9
  robdockins

  committed
  db984b9

  Copy full SHA for db984b9

• typo

  robdockins

  committed
  e298ac0

  Copy full SHA for e298ac0

• Add some additional comments on the advisory "inhabited" flag

  Show description for 53cacf1
  robdockins

  committed
  53cacf1

  Copy full SHA for 53cacf1