von Coq importiert

Question

Kann jemand bitte sagen Sie mir, die Unterschiede zwischen

• RequireNamen.
• Require ImportName.
• ImportNamen

?

Answer 1

• Require: eine externe Bibliothek geladen werden (in der Regel aus der Standardbibliothek oder user-contribs/ folder);
• Import: importiert die Namen in einem Modul. Wenn Sie zum Beispiel eine Funktion f in einem Modul M haben, indem Sie Import M. tun, müssen Sie nur f statt M.f eingeben;
• Require Import: funktioniert sowohl Require als auch Import.