Title: Theory / Unimportant / CS / Programming / Coq / Vernacular
Tags: FromInstruction algoToProg computer_to_instruction hasNotNewEffectReturnsMeaning declaration some_instruction

Instruction: Example/Theorem/Lemma/Remark/Fact foo: bar
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Effect: Create an assertion named foo whose value is bar
Language: coq
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Extra: prog

Instruction: Definition foo bar:bing :=
  buz
end.
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Meaning: Define a function with parameter(s) bar whose value is buz
Language: coq
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Identifier: foo
Typ: function returning a value of type bing
Extra: prog

Instruction: Notation "foo" := bar
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Effect: Introduce foo as a notation representing bar
Language: coq
Context: Coq
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Extra: prog

Instruction: _
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Effect: A place holder for an argument
Language: coq
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Extra: prog

Instruction: M.F
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Effect: Accessing the element F of M
Language: coq
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Variables: M a module
F in M
Extra: prog

Instruction: Fixpoint foo bar:=
  buz
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Meaning: Define a function foo with parameters bar, executing buz where foo's value is the currently defined function
Language: coq
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Identifier: foo
Assuming: each call to foo in buz is made on an argument smaller than bar
Extra: prog

Instruction: forall. foo:bar, buz
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Effect: The formula stating that, for every value foo of type bar, buz holds
Language: coq
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Extra: prog

Instruction: foo -> bar
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Effect: assuming foo, bar holds
Language: coq
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Extra: prog

Instruction: match buz with
  | bar_1: => foo_1
  ...
  | bar_n =>foo_n
Page: prog
https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Effect: The value is foo_i when the value of the variable buz is equal to bar_i.
Language: coq
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Extra: prog

Instruction: Type_ind
Page: 41
Effect: ∀ P : Type → Prop, P case_1, ...., P case_n → ∀ x : Type, P x
Language: coq
Chapter: 3
Section: 1
Variables: Inductive Type: Class :=
  | case_1
  | ...
  | case_n.