diff options
| author | Son Ho | 2023-07-12 18:04:19 +0200 |
|---|---|---|
| committer | Son Ho | 2023-07-12 18:04:19 +0200 |
| commit | eb97bdb6761437e492bcf1a95b4fa43d2b69601b (patch) | |
| tree | 666cf4611365dea7d9d7240870e8acbcb8dc5a4d /backends/lean/Base/Progress/Base.lean | |
| parent | e010c10fb9a1e2d88b52a4f6b4a0865448276013 (diff) | |
Improve progress to use assumptions and start working on a nice syntax
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base/Progress/Base.lean | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean index 613f38f8..a288d889 100644 --- a/backends/lean/Base/Progress/Base.lean +++ b/backends/lean/Base/Progress/Base.lean @@ -60,7 +60,7 @@ section Methods trace[Progress] "Theorem: {th}" -- Dive into the quantified variables and the assumptions forallTelescope th fun fvars th => do - trace[Progress] "All argumens: {fvars}" + trace[Progress] "All arguments: {fvars}" /- -- Filter the argumens which are not propositions let rec getFirstPropIdx (i : Nat) : MetaM Nat := do if i ≥ fargs.size then pure i |