Commit 7d981af6 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix `Export` order for `length`. Remove `length` hack in strings. Add a test.

parent 4b0c93cb
Pipeline #26356 failed with stage
in 10 minutes and 16 seconds
length : ∀ A : Type, list A → nat
length is not universe polymorphic
Arguments length {A}%type_scope _%list_scope
length is transparent
Expands to: Constant Coq.Init.Datatypes.length
length : ∀ A : Type, list A → nat
length is not universe polymorphic
Arguments length {A}%type_scope _%list_scope
length is transparent
Expands to: Constant Coq.Init.Datatypes.length
length : ∀ A : Type, list A → nat
length is not universe polymorphic
Arguments length {A}%type_scope _%list_scope
length is transparent
Expands to: Constant Coq.Init.Datatypes.length
(** Check that we always get the [length] function on lists, not on strings. *)
From stdpp Require Import prelude.
About length.
From stdpp Require Import strings.
About length.
From stdpp Require Import prelude.
About length.
\ No newline at end of file
......@@ -3,7 +3,12 @@ that are used throughout the whole development. Most importantly it contains
abstract interfaces for ordered structures, sets, and various other data
structures. *)
From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
(** The order of this [Require Export] is important: The definition of [length]
in [List] should shadow the definition of [length] in [String]. We also need
to export [Datatypes] because [List] contains a [parsing only] notation for
[length], not the actual definition of [length], which is in [Datatypes]. *)
From Coq Require Export String Datatypes List.
From Coq Require Export Morphisms RelationClasses Bool Utf8 Setoid.
From Coq Require Import Permutation.
Set Default Proof Using "Type".
Export ListNotations.
......
From Coq Require Import Ascii.
From Coq Require Export String.
From stdpp Require Export list.
From stdpp Require Import countable.
Set Default Proof Using "Type".
(* To avoid randomly ending up with String.length because this module is
imported hereditarily somewhere. *)
Notation length := List.length.
(** * Fix scopes *)
Open Scope string_scope.
(* Make sure [list_scope] has priority over [string_scope], so that
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment