← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to test/fail/Interaction-and-input-file.err

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
test/fail/Interaction-and-input-file.err
1
 
Error: Choose at most one: input file or --interaction.
2
 
 
3
 
Agda
4
 
 
5
 
Usage: agda [OPTIONS...] [FILE]
6
 
 
7
 
  -V      --version                                   show version number
8
 
  -?      --help                                      show this help
9
 
  -I      --interactive                               start in interactive mode
10
 
          --interaction                               for use with the Emacs mode
11
 
  -c      --compile                                   compile program using the MAlonzo backend (experimental)
12
 
          --epic                                      compile program using the Epic backend
13
 
          --js                                        compile program using the JS backend
14
 
          --compile-dir=DIR                           directory for compiler output (default: the project root)
15
 
          --ghc-flag=GHC-FLAG                         give the flag GHC-FLAG to GHC when compiling using MAlonzo
16
 
          --epic-flag=EPIC-FLAG                       give the flag EPIC-FLAG to Epic when compiling using Epic
17
 
          --test                                      run internal test suite
18
 
          --vim                                       generate Vim highlighting files
19
 
          --latex                                     generate LaTeX with highlighted source code
20
 
          --latex-dir=DIR                             directory in which LaTeX files are placed (default: latex)
21
 
          --html                                      generate HTML files with highlighted source code
22
 
          --dependency-graph=FILE                     generate a Dot file with a module dependency graph
23
 
          --html-dir=DIR                              directory in which HTML files are placed (default: html)
24
 
          --css=URL                                   the CSS file used by the HTML files (can be relative)
25
 
          --ignore-interfaces                         ignore interface files (re-type check everything)
26
 
  -i DIR  --include-path=DIR                          look for imports in DIR
27
 
          --no-forcing                                disable the forcing optimisation
28
 
          --safe                                      disable postulates, unsafe OPTION pragmas and primTrustMe
29
 
          --show-implicit                             show implicit arguments when printing
30
 
          --show-irrelevant                           show irrelevant arguments when printing
31
 
  -v N    --verbose=N                                 set verbosity level to N
32
 
          --allow-unsolved-metas                      allow unsolved meta variables (only needed in batch mode)
33
 
          --no-positivity-check                       do not warn about not strictly positive data types
34
 
          --no-termination-check                      do not warn about possibly nonterminating code
35
 
          --termination-depth=N                       allow termination checker to count decrease/increase upto N (default N=1)
36
 
          --no-coverage-check                         do not warn about possibly incomplete pattern matches
37
 
          --type-in-type                              ignore universe levels (this makes Agda inconsistent)
38
 
          --sized-types                               use sized types (inconsistent with coinduction)
39
 
          --injective-type-constructors               enable injective type constructors (makes Agda anti-classical and possibly inconsistent)
40
 
          --guardedness-preserving-type-constructors  treat type constructors as inductive constructors when checking productivity
41
 
          --no-universe-polymorphism                  disable universe polymorphism
42
 
          --universe-polymorphism                     enable universe polymorphism (default)
43
 
          --no-irrelevant-projections                 disable projection of irrelevant record fields
44
 
          --experimental-irrelevance                  enable potentially unsound irrelevance features (irrelevant levels, irrelevant data matching)
45
 
          --without-K                                 disable the K rule (maybe)
46
 
          --copatterns                                enable definitions by copattern matching
47
 
 
48
 
Plugins: