summaryrefslogtreecommitdiff
path: root/backends/lean
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean')
-rw-r--r--backends/lean/Base/Primitives/CoreConvertNum.lean1
-rw-r--r--backends/lean/Base/Primitives/ScalarNotations.lean33
-rw-r--r--backends/lean/Base/Primitives/Vec.lean4
3 files changed, 22 insertions, 16 deletions
diff --git a/backends/lean/Base/Primitives/CoreConvertNum.lean b/backends/lean/Base/Primitives/CoreConvertNum.lean
index eb456a96..b53d11db 100644
--- a/backends/lean/Base/Primitives/CoreConvertNum.lean
+++ b/backends/lean/Base/Primitives/CoreConvertNum.lean
@@ -4,6 +4,7 @@ import Init.Data.List.Basic
import Mathlib.Tactic.Linarith
import Base.IList
import Base.Primitives.Scalar
+import Base.Primitives.ScalarNotations
import Base.Primitives.ArraySlice
import Base.Arith
import Base.Progress.Base
diff --git a/backends/lean/Base/Primitives/ScalarNotations.lean b/backends/lean/Base/Primitives/ScalarNotations.lean
index cc6e6f02..94c0c779 100644
--- a/backends/lean/Base/Primitives/ScalarNotations.lean
+++ b/backends/lean/Base/Primitives/ScalarNotations.lean
@@ -8,20 +8,18 @@ namespace Primitives
open Lean Meta Elab Term
-macro x:term:max "#isize" : term => `(Isize.ofInt $x (by scalar_tac))
-macro x:term:max "#i8" : term => `(I8.ofInt $x (by scalar_tac))
-macro x:term:max "#i16" : term => `(I16.ofInt $x (by scalar_tac))
-macro x:term:max "#i32" : term => `(I32.ofInt $x (by scalar_tac))
-macro x:term:max "#i64" : term => `(I64.ofInt $x (by scalar_tac))
-macro x:term:max "#i128" : term => `(I128.ofInt $x (by scalar_tac))
-macro x:term:max "#usize" : term => `(Usize.ofInt $x (by scalar_tac))
-macro x:term:max "#u8" : term => `(U8.ofInt $x (by scalar_tac))
-macro x:term:max "#u16" : term => `(U16.ofInt $x (by scalar_tac))
-macro x:term:max "#u32" : term => `(U32.ofInt $x (by scalar_tac))
-macro x:term:max "#u64" : term => `(U64.ofInt $x (by scalar_tac))
-macro x:term:max "#u128" : term => `(U128.ofInt $x (by scalar_tac))
-
-macro x:term:max noWs "u32" : term => `(U32.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#isize" : term => `(Isize.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#i8" : term => `(I8.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#i16" : term => `(I16.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#i32" : term => `(I32.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#i64" : term => `(I64.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#i128" : term => `(I128.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#usize" : term => `(Usize.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#u8" : term => `(U8.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#u16" : term => `(U16.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#u32" : term => `(U32.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#u64" : term => `(U64.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#u128" : term => `(U128.ofInt $x (by scalar_tac))
-- Notation for pattern matching
-- We make the precedence looser than the negation.
@@ -87,4 +85,11 @@ example : Result Usize := 0#usize + 1#usize
-- More complex expressions
example (x y : Int) (h : 0 ≤ x + y ∧ x + y ≤ 1000) : U32 := (x + y)#u32
+section Scalar.Examples
+abbrev NList (a : Type) (x : U32) := { l : List a // l.length = x.val }
+
+example : NList Int 0#u32 := ⟨ [], by simp ⟩
+
+end Scalar.Examples
+
end Primitives
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 5ed7b606..d144fcb8 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -34,7 +34,7 @@ abbrev Vec.v {α : Type u} (v : Vec α) : List α := v.val
example {a: Type u} (v : Vec a) : v.length ≤ Scalar.max ScalarTy.Usize := by
scalar_tac
-def Vec.new (α : Type u): Vec α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp; decide ⟩
+def Vec.new (α : Type u): Vec α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩
instance (α : Type u) : Inhabited (Vec α) := by
constructor
@@ -192,7 +192,7 @@ def alloc.slice.Slice.to_vec
def core.slice.Slice.reverse (T : Type) (s : Slice T) : Slice T :=
⟨ s.val.reverse, by sorry ⟩
-def alloc.vec.Vec.with_capacity (T : Type) (s : Usize) : alloc.vec.Vec T := Vec.new T
+def alloc.vec.Vec.with_capacity (T : Type) (_ : Usize) : alloc.vec.Vec T := Vec.new T
/- [alloc::vec::{(core::ops::deref::Deref for alloc::vec::Vec<T, A>)#9}::deref]:
Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/vec/mod.rs', lines 2624:4-2624:27