Joachim Breitner 7d60d8b563 feat: safer #eval, and #eval! (#4810) ... previously, `#eval` would happily evaluate expressions that contain `sorry`, either explicitly or because of failing tactics. In conjunction with operations like array access this can lead to the lean process crashing, which isn't particularly great. So how `#eval` will refuse to run code that (transitively) depends on the `sorry` axiom (using the same code as `#print axioms`). If the user really wants to run it, they can use `#eval!`. Closes #1697		2024-07-23 15:26:56 +00:00
..
bin	chore: update domain	2023-09-20 15:13:27 -07:00
dev	doc: update release checklist for new release notes workflow (#4458)	2024-07-09 21:44:15 +00:00
examples	feat: safer #eval, and #eval! (#4810)	2024-07-23 15:26:56 +00:00
images	doc: update quickstart guide (#4806)	2024-07-23 07:31:21 +00:00
latex	doc: upstream the Lean4 pygments lexer (#3125)	2024-05-20 11:40:24 +00:00
make	doc: updated build instructions for mac os X (#4317)	2024-06-01 16:23:17 +00:00
monads	chore: Std -> Batteries renaming (#4108)	2024-05-08 05:04:25 +00:00
.gitignore
alectryon.css	doc: fix overwide view when using Alectryon	2022-06-23 18:23:28 +02:00
alectryon.js	doc: embed examples into doc book	2022-04-06 09:06:49 -07:00
array.md	doc: add new example	2022-07-09 17:04:08 -07:00
autobound.md	doc: Semantic highlighting	2022-10-02 08:37:15 -07:00
book.toml	doc: fold sub-chapters by default	2022-04-20 18:46:30 +02:00
bool.md	chore: CRLF be gone	2021-11-09 09:49:09 +01:00
BoolExpr.lean	chore: Std -> Batteries renaming (#4108)	2024-05-08 05:04:25 +00:00
builtintypes.md
char.md	doc: documenting Char and upstreaming extensionality from batteries (#4438)	2024-06-16 00:43:34 +00:00
declarations.md	doc: mention termination_by and decreasing_by (#3016)	2024-01-10 16:35:19 +00:00
decltypes.md
definitions.md
dep.md
deptypes.md
do.md	doc: document some do block patterns/sugar	2022-02-07 20:50:15 +01:00
elaborators.md	doc: clean up syntax ToC	2022-04-26 18:58:45 +02:00
enum.md
examples.md	doc: embed examples into doc book	2022-04-06 09:06:49 -07:00
expressions.md	doc: fix typos (#2160)	2023-03-22 10:01:59 +01:00
faq.md	doc: fix the link to contribution guidelines (#2623)	2023-10-05 12:02:55 +11:00
flake.lock	feat: partial context info (#3159)	2024-01-22 12:34:20 +00:00
flake.nix	chore: test results as job summary (#3715)	2024-03-27 10:14:33 +00:00
float.md
fplean.md	chore: update domain	2023-09-20 15:13:27 -07:00
funabst.md
functions.md	fix: broken internal links in the docs (#3216)	2024-01-25 09:56:20 +00:00
highlight.js	fix: highlight of deriving instance (#1717)	2022-10-12 14:24:16 -07:00
implicit.md	chore: prune ancient keywords	2022-08-01 13:32:56 +02:00
inductive.md	chore: update domain	2023-09-20 15:13:27 -07:00
int.md	doc: fix integer division example	2024-07-19 10:36:43 +02:00
introdef.md
lean3changes.md	chore: expand remark	2023-05-05 12:21:32 -07:00
lexical_structure.md	feat: Rust-style raw string literals (#2929)	2023-12-20 16:53:08 +00:00
list.md
macro_overview.md	doc: fix typos (#2160)	2023-03-22 10:01:59 +01:00
metaprogramming-arith.lean	refactor: remove some unnecessary antiquotation kind annotations	2022-07-23 17:09:32 +02:00
metaprogramming-arith.md	doc: update link target (#3218)	2024-01-26 10:20:22 +00:00
mission.md	doc: start porting reference manual	2021-08-27 19:30:08 -07:00
namespaces.md
nat.md
notation.md	feat: reduce precedence of unary neg	2022-11-06 18:13:48 -08:00
option.md
organization.md
other_commands.md	doc: fix some syntax and link in the docs, and more	2021-10-10 11:36:43 +02:00
perf.md	doc: add basic perf documentation	2021-09-06 07:12:36 -07:00
pygments.css	doc: add documentation on monads (#1505)	2022-09-05 13:33:15 -07:00
quickstart.md	doc: update quickstart guide (#4806)	2024-07-23 07:31:21 +00:00
sections.md
semantic_highlighting.md	chore: update domain	2023-09-20 15:13:27 -07:00
setup.md	chore: CI: native-compile aarch64 macOS (#4265)	2024-05-24 08:18:49 +00:00
simptypes.md
string.md
stringinterp.md
struct.md	doc: structure update	2021-12-15 11:48:46 +00:00
SUMMARY.md	feat: checklist for release process (#3536)	2024-03-05 02:55:17 +00:00
syntax.md	doc: clean up syntax ToC	2022-04-26 18:58:45 +02:00
syntax_example.lean	doc: fix example style	2022-04-22 16:26:16 +02:00
syntax_example.md	doc: fix example style	2022-04-22 16:26:16 +02:00
syntax_examples.md	doc: missing file	2022-04-20 19:13:53 +02:00
syntax_highlight_in_latex.md	doc: upstream the Lean4 pygments lexer (#3125)	2024-05-20 11:40:24 +00:00
tactics.md	doc: fix typos (#2160)	2023-03-22 10:01:59 +01:00
task.md
thunk.md	doc: fix trivial typo	2022-01-09 10:19:26 +01:00
tour.md	fix: broken internal links in the docs (#3216)	2024-01-25 09:56:20 +00:00
tpil.md	chore: update domain	2023-09-20 15:13:27 -07:00
typeclass.md	doc: avoid universe issue in example type class code (#3098)	2023-12-21 16:57:26 +00:00
typeobjs.md
types.md	chore: CRLF be gone	2021-11-09 09:49:09 +01:00
uint.md
unifhint.md
using_lean.md	doc: start porting reference manual	2021-08-27 19:30:08 -07:00
whatIsLean.md	fix: broken internal links in the docs (#3216)	2024-01-25 09:56:20 +00:00