moon/zygotec - work-in-progress programming language.

	Commit message (Collapse)	Author	Age	Files	Lines
*	prover: do not restore length facts after a call-loop	zinc	13 days	1	-3/+5
\| \| \| \| \| \| \|	Restoring undirtied lafacts when the body might free was wrong: push can grow an array without dirtying its name, so a[99] after push warned against a stale length 0. Keep the old lafact_keep rule; reorder explain_prover so the constant/affine cases run before the touch() loops.
*	wip: prover gaps (inline len bound, cross-array, rt.new depth, fixed new, ↵	zinc	13 days	1	-0/+40
	affine i*n+k); unbuilt and untested