Stream: Coq users

Topic: How to Tell Coq to Use Length from Different Import


view this post on Zulip Julia Dijkstra (Jan 09 2024 at 10:27):

Coq currently thinks I want to use the length fixpoint from a strings import, but I actually would like to use length from my lists import. I currently use List.length, but since I don't use string length, is there a way to tell Coq to simply use length for lists?

view this post on Zulip Julia Dijkstra (Jan 09 2024 at 10:32):

I can hack this in, but I am pretty sure this is not how you're supposed to do this :sweat_smile: .

Definition length {X: Type} (l: list X): nat := List.length l.

view this post on Zulip Kenji Maillard (Jan 09 2024 at 10:42):

You can select which function you want to refer to with the identifier list by modifying the order of Import. Moreover you can selectively re-import the function length at any point:

From Coq Require Import List String.

Locate length.
(* Constant Coq.Strings.String.length *)
(* Constant Coq.Init.Datatypes.length *)
(*   (shorter name to refer to it in current context is Datatypes.length) *)
(* Notation Coq.Lists.List.length *)
(*   (shorter name to refer to it in current context is List.length) *)

Import List(length).

Locate length.
(* Notation Coq.Lists.List.length *)
(* Constant Coq.Init.Datatypes.length *)
(*   (shorter name to refer to it in current context is Datatypes.length) *)
(* Constant Coq.Strings.String.length *)
(*   (shorter name to refer to it in current context is String.length) *)

Last updated: Jun 22 2024 at 15:01 UTC