Julian/README.md Secret

## README.md

      
    Raw
  

              README.md
            
          
Logical symbol
Appears in goal
Appears in hypothesis


∀  (for all)
intro new_name
apply expr or specialize name expr                                                     


∃  (there exists)
use expr
cases expr with 
  | intro new_name new_name => ...                                


→  (implies)
intro new_name
apply expr or specialize name expr                                                     


↔  (if and only if)
constructor
rw [expr] or rw [← expr]                                                                 


∧  (and)
constructor
cases expr with 
  | intro new_name new_name => ...                                


∨  (or)
left or right
cases expr with 
  | inl new_name => ... 
  | inr new_name => ... 


¬  (not)
intro new_name
apply expr or specialize name expr
Logical symbol	Appears in goal	Appears in hypothesis
`∀` (for all)	`intro new_name`	`apply expr` or `specialize name expr`
`∃` (there exists)	`use expr`	`cases expr with` `\| intro new_name new_name => ...`
`→` (implies)	`intro new_name`	`apply expr` or `specialize name expr`
`↔` (if and only if)	`constructor`	`rw [expr]` or `rw [← expr]`
`∧` (and)	`constructor`	`cases expr with` `\| intro new_name new_name => ...`
`∨` (or)	`left` or `right`	`cases expr with` `\| inl new_name => ...` `\| inr new_name => ...`
`¬` (not)	`intro new_name`	`apply expr` or `specialize name expr`