diff options
Diffstat (limited to 'test-suite/output/InitSyntax.out')
| -rw-r--r-- | test-suite/output/InitSyntax.out | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out new file mode 100644 index 0000000000..c17c63e724 --- /dev/null +++ b/test-suite/output/InitSyntax.out @@ -0,0 +1,12 @@ +Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := + exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x} + +For sig2: Argument A is implicit +For exist2: Argument A is implicit +For sig2: Argument scopes are [type_scope type_scope type_scope] +For exist2: Argument scopes are [type_scope function_scope function_scope _ _ + _] +exists x : nat, x = x + : Prop +fun b : bool => if b then b else b + : bool -> bool |
