diff options
| -rw-r--r-- | coq.html.markdown | 8 | ||||
| -rw-r--r-- | de-de/nix-de.html.markdown | 3 |
2 files changed, 7 insertions, 4 deletions
diff --git a/coq.html.markdown b/coq.html.markdown index 4c1ad690..3a924a19 100644 --- a/coq.html.markdown +++ b/coq.html.markdown @@ -61,8 +61,8 @@ Locate "+". (* Calling a function with insufficient number of arguments does not cause an error, it produces a new function. *) -Definition make_inc x y := x + y. (* make_inc is int -> int -> int *) -Definition inc_2 := make_inc 2. (* inc_2 is int -> int *) +Definition make_inc x y := x + y. (* make_inc is nat -> nat -> nat *) +Definition inc_2 := make_inc 2. (* inc_2 is nat -> nat *) Compute inc_2 3. (* Evaluates to 5 *) @@ -370,7 +370,7 @@ Close Scope string_scope. power series and results,...) • Relations : Relations (definitions and basic results) • Sorting : Sorted list (basic definitions and heapsort correctness) -• Strings : 8-bits characters and strings +• Strings : 8-bit characters and strings • Wellfounded : Well-founded relations (basic results) *) @@ -472,7 +472,7 @@ Proof. intros A B ab. destruct ab as [ a b ]. apply a. Qed. -(* We can prove easily prove simple polynomial equalities using the +(* We can easily prove simple polynomial equalities using the automated tactic ring. *) Require Import Ring. diff --git a/de-de/nix-de.html.markdown b/de-de/nix-de.html.markdown index ea02e81d..ffe8dffc 100644 --- a/de-de/nix-de.html.markdown +++ b/de-de/nix-de.html.markdown @@ -356,3 +356,6 @@ with builtins; [ * [Susan Potter - Nix Cookbook - Nix By Example] (https://ops.functionalalgebra.com/nix-by-example/) + +* [Rommel Martinez - A Gentle Introduction to the Nix Family] + (https://web.archive.org/web/20210121042658/https://ebzzry.io/en/nix/#nix) |