From 4e3f9fa045cc232ee05c314dced98a473bccaf63 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 13 Jan 2025 08:06:28 +0100 Subject: [PATCH] chore: updated progress tracker --- Manual.lean | 115 +++++++++++++++++++++++++++++++++++++++------ lake-manifest.json | 2 +- 2 files changed, 101 insertions(+), 16 deletions(-) diff --git a/Manual.lean b/Manual.lean index 53eb830..c11f412 100644 --- a/Manual.lean +++ b/Manual.lean @@ -156,14 +156,37 @@ file := some "the-index" :::progress ```namespace List +Int +IntCast Function -Functor Applicative Monad Pure Bind Seq SeqLeft SeqRight -MonadState MonadStateOf StateT StateM -MonadReader MonadReaderOf ReaderT ReaderM -MonadExcept MonadExceptOf ExceptT Except -MonadFunctor MonadFunctorT -MonadControl MonadControlT -MonadLift MonadLiftT +Ord +Ordering +Functor +Applicative +Monad +Pure +Bind +Seq +SeqLeft +SeqRight +MonadState +MonadStateOf +StateT +StateM +MonadReader +MonadReaderOf +ReaderT +ReaderM +MonadExcept +MonadExceptOf +ExceptT +Except +MonadFunctor +MonadFunctorT +MonadControl +MonadControlT +MonadLift +MonadLiftT OptionT StateRefT' StateCpsT @@ -176,18 +199,80 @@ ForM ForIn ForInStep ForIn' -EStateM EStateM.Result EStateM.Backtrackable -String Char Nat Lean.Elab.Tactic Array Subarray IO IO.FS System System.FilePath IO.Process IO.FS.Stream ST IO.Error IO.FS.Stream.Buffer IO.FS.Handle -IO.Process.SpawnArgs IO.Process.Output IO.Process.Child IO.Process.StdioConfig IO.Process.Stdio IO.Ref ST.Ref IO.FS.Metadata IO.FS.DirEntry EIO BaseIO -IO.FileRight IO.FS.Stream Task Task.Priority Unit PUnit -Bool Decidable +EStateM +EStateM.Result +EStateM.Backtrackable +String +Char +Nat +Lean.Elab.Tactic +Array +Subarray +IO +IO.FS +System +System.FilePath +IO.Process +IO.FS.Stream +ST +IO.Error +IO.FS.Stream.Buffer +IO.FS.Handle +IO.Process.SpawnArgs +IO.Process.Output +IO.Process.Child +IO.Process.StdioConfig +IO.Process.Stdio +IO.Ref +ST.Ref +IO.FS.Metadata +IO.FS.DirEntry +EIO +BaseIO +IO.FileRight +IO.FS.Stream +Task +Task.Priority +Unit +PUnit +Bool +Decidable System.Platform -PLift ULift Subtype Option List +PLift +ULift +Subtype +Option +List USize -UInt8 UInt16 UInt32 UInt64 +UInt8 +UInt16 +UInt32 +UInt64 ISize -Int8 Int16 Int32 Int64 +Int8 +Int16 +Int32 +Int64 Fin +Option +List +Prod +PProd +MProd +Sum +PSum +Sigma +Subtype +Thunk +_root_ +BitVec +Float +Empty +Quotient +Quot +Setoid +Squash +Subsingleton ``` ```exceptions diff --git a/lake-manifest.json b/lake-manifest.json index 889f587..a3677a4 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "7e93d5b3dd3d083e7824a7559cd8a8dec49265bc", + "rev": "973eb19cffaf09731f1a8d24d36819687a06f251", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "main",