generated from amazon-archives/__template_Apache-2.0
-
Notifications
You must be signed in to change notification settings - Fork 23
Open
Description
The random LExpr generator in Strata/DL/Lambda/TestGen.lean fails sometimes. Specifically, it is this test:
let P : LExpr TrivialParams.mono → Prop := fun t => HasType example_lctx example_ctx t example_ty
let t ← Gen.runUntil (.some 1) (ArbitrarySizedSuchThat.arbitrarySizedST P 5) 5
IO.println s!"Generated {t}"
The reason must be identified. #327 makes the test successful by fixing the random seed.
Metadata
Metadata
Assignees
Labels
No labels