Merge pull request #51 from argumentcomputer/ap/4-16-0

chore: update to Lean v4.16.0

CI.lean

@@ -13,7 +13,7 @@ jobs:
       - name: install elan
         run: |
           set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v4.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
           ./elan-init -y --default-toolchain none
           echo \"$HOME/.elan/bin\" >> $GITHUB_PATH
       - uses: actions/checkout@v2

LSpec/LSpec.lean

@@ -6,7 +6,8 @@ import LSpec.SlimCheck.Checkable
 # The core `LSpec` framework
 
 ## Add all relavent documentation
-Check [here](./LSpec/Examples.lean) for examples of uses 
+
+Check [here](./LSpec/Examples.lean) for examples of uses
 
 ## Tags
 
@@ -15,13 +16,12 @@ testing frameworks
 ## References
 
   * https://hackage.haskell.org/package/hspec
-
 -/
 
 namespace LSpec
 
 /--
-The main typeclass of propositions that can be tested by `LSpec`. 
+The main typeclass of propositions that can be tested by `LSpec`.
 
 In non-succeeding cases, it may contain an explanatory message.
 -/
@@ -90,7 +90,7 @@ def group (descr : String) (groupTests : TestSeq)
   .group descr groupTests next
 
 open SlimCheck Decorations in
-/-- 
+/--
 Checks a `Checkable` prop. Note that `mk_decorations` is here simply to improve error messages
 and if `p` is Checkable, then so is `p'`.
 -/

LSpec/SlimCheck/Control/DefaultRange.lean

@@ -7,19 +7,19 @@ Authors: Hanting Zhang
 /-!
 # Bounded and DefaultRange classes
 
-This module encapsulates the notion of a range of elements. 
+This module encapsulates the notion of a range of elements.
 
 ## Main definitions
-  * `Bounded` class for objects which are naturally bounded 
+  * `Bounded` class for objects which are naturally bounded
     by two `lo` and `hi` elements;
-  * `DefaultRange` class for objects which are unbounded, 
+  * `DefaultRange` class for objects which are unbounded,
     but nevertheless need a convenient range of values which to operate within.
 
-Note that we go against Lean's principles by NOT providing any 
-mathematical guarantees for the `Bounded` and `DefaultRange` classes. 
+Note that we go against Lean's principles by NOT providing any
+mathematical guarantees for the `Bounded` and `DefaultRange` classes.
 It is perfectly possible to define `Bounded Nat` with `lo := 37` and `hi := 37`;
 we leave these to the judgement of the programmer. *gasp of horror*
-This more follows the design of `Bounded` in Haskell, and allows us to 
+This more follows the design of `Bounded` in Haskell, and allows us to
 forgo carrying proofs around when we start defining `Random` instances.
 
 Lean developers, please forgive us.
@@ -30,31 +30,31 @@ Lean developers, please forgive us.
 
 namespace SlimCheck
 
-class Bounded (α : Type u) where 
+class Bounded (α : Type u) where
   lo : α
   hi : α
 
-class DefaultRange (α : Type u) where 
+class DefaultRange (α : Type u) where
   lo : α
   hi : α
 
-instance [Bounded α] : DefaultRange α where 
-  lo := Bounded.lo 
+instance [Bounded α] : DefaultRange α where
+  lo := Bounded.lo
   hi := Bounded.hi
 
-instance : Bounded Bool where 
-  lo := true 
-  hi := false
+instance : Bounded Bool where
+  lo := false
+  hi := true
 
-instance : DefaultRange Nat where 
-  lo := 0 
+instance : DefaultRange Nat where
+  lo := 0
   hi := USize.size
 
-instance {n : Nat} : Bounded (Fin n.succ) where 
+instance {n : Nat} : Bounded (Fin n.succ) where
   lo := ⟨0, n.succ_pos⟩
   hi := ⟨n, n.lt_succ_self⟩
 
-instance : DefaultRange Int where 
+instance : DefaultRange Int where
   lo :=  - Int.ofNat (USize.size / 2)
   hi := Int.ofNat (USize.size / 2 - 1)
 

LSpec/Testing.lean

@@ -105,4 +105,4 @@ section slimcheck_tests
 -------------------
 -- ? mul_comm
 
-end slimcheck_tests
+end slimcheck_tests

lake-manifest.json

@@ -1,4 +1,4 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages": [],
  "name": "LSpec",

lakefile.toml

@@ -0,0 +1,14 @@
+name = "LSpec"
+version = "1.0.0"
+defaultTargets = ["lspec"]
+
+[[lean_lib]]
+name = "LSpec"
+
+[[lean_exe]]
+name = "lspec"
+root = "Main"
+
+[[lean_exe]]
+name = "lspec-ci"
+root = "CI"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.14.0
+leanprover/lean4:v4.16.0