fix(tests/lean): subtype notation is not in the top-level anymore
This commit is contained in:
parent
c52ffda0e0
commit
fe66e2aa4a
7 changed files with 7 additions and 5 deletions
|
@ -1,5 +1,5 @@
|
|||
import data.pnat
|
||||
open pnat
|
||||
open pnat subtype
|
||||
|
||||
print pnat
|
||||
|
||||
|
|
|
@ -1 +1,2 @@
|
|||
open subtype
|
||||
print axioms
|
||||
|
|
|
@ -1 +1 @@
|
|||
print axioms
|
||||
open subtype print axioms
|
||||
|
|
|
@ -1,3 +1,4 @@
|
|||
open subtype
|
||||
theorem foo1 : 0 = (0:num) :=
|
||||
rfl
|
||||
|
||||
|
|
|
@ -1,3 +1,3 @@
|
|||
import data.nat
|
||||
open nat
|
||||
open nat subtype
|
||||
check { x : nat | x > 0}
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
-- import data.subtype
|
||||
open nat
|
||||
open nat subtype
|
||||
|
||||
check {x : nat| x > 0 }
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
example (f : nat → nat) (a b : nat) : f a = a → f (f a) = a :=
|
||||
open subtype example (f : nat → nat) (a b : nat) : f a = a → f (f a) = a :=
|
||||
begin
|
||||
intro h₁,
|
||||
subst h₁ -- ERROR
|
||||
|
|
Loading…
Reference in a new issue