lean2/tests/lean/run/sub_bug.lean

3 lines
58 B
Text

import data.nat
open nat subtype
check { x : nat | x > 0}