Moogle Input Syntax

• locate <pattern>

  <pattern> is a shell like pattern which could include * (denoting any sequence of 0 or more characters) and ? (denoting any single character).
  

  Examples:

  • nat pattern matches cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1) only
  • n?t pattern matches cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1) and cic:/Coq/Init/Logic/not.con
  • nat* pattern matches cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1), cic:/Coq/Init/Peano/nat_case.con and many more

• hint
• match
• elim