Jon Sterling on Nostr: Some strange behaviour with Lean's evaluation of thunks. I wonder if is intentional ...
Some strange behaviour with Lean's evaluation of thunks. I wonder if is intentional that this result in [[forcing]] being printed twice?
Keep in mind that if I do a variation on this without using an inductive type constructor, [[forcing]] is printed only once.
#Lean4 #Lean
Published at
2025-02-16 13:53:39Event JSON
{
"id": "214b9112ea89ddc86f14bd9d0e999118a70f80abd73ecff9673860d3d2514d3d",
"pubkey": "ba51d3bb7fc92891016b5873c0b4f7c6a0550c964ec565ece24b6fc2dcf93301",
"created_at": 1739714019,
"kind": 1,
"tags": [
[
"t",
"lean"
],
[
"t",
"Lean4"
],
[
"imeta",
"url https://media.mathstodon.xyz/media_attachments/files/114/013/893/868/911/371/original/17305ae2d7a392bd.png",
"m image/png",
"dim 1140x942",
"blurhash U5S?DW02IWohWBRkWFWCW?WCoJWB-=RnM|WY"
],
[
"proxy",
"https://mathstodon.xyz/users/jonmsterling/statuses/114013897954189956",
"activitypub"
]
],
"content": "Some strange behaviour with Lean's evaluation of thunks. I wonder if is intentional that this result in [[forcing]] being printed twice?\n\nKeep in mind that if I do a variation on this without using an inductive type constructor, [[forcing]] is printed only once.\n\n#Lean4 #Lean\n\nhttps://media.mathstodon.xyz/media_attachments/files/114/013/893/868/911/371/original/17305ae2d7a392bd.png",
"sig": "17c699a165bee9c43506176dcb6aa2446f591cca5f3650283f91fa046cfbb2825e458fc1f83f7d669609f5ebac9257265bf041d03d723984ae6d06024ebe6b28"
}
