Title: Theory / Unimportant / CS / Programming / Coq / Gallina

Instruction: if value then bar_1 else bar_2
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Language: coq
Returns: bar_1 if value uses constructor_1, bar_2 otherwise
Assuming: Inductive Type : Class :=
  | constructor_1 ...
  | constructor_2 ...
value: Type

Name: A proof term
Definition: A gallina term of logical type
Page: 41
Chapter: 3
Section: 1
Context: coq