Commit 53189fab authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' of https://gitlab.mpi-sws.org/iris/stdpp

parents b776e361 17241997
Pipeline #14024 passed with stage
in 16 minutes and 1 second
......@@ -241,12 +241,12 @@ Definition equivL {A} : Equiv A := (=).
(** A [Params f n] instance forces the setoid rewriting mechanism not to
rewrite in the first [n] arguments of the function [f]. We will declare such
instances for all operational type classes in this development. *)
Instance: Params (@equiv) 2.
Instance: Params (@equiv) 2 := {}.
(** The following instance forces [setoid_replace] to use setoid equality
(for types that have an [Equiv] instance) rather than the standard Leibniz
equality. *)
Instance equiv_default_relation `{Equiv A} : DefaultRelation () | 3.
Instance equiv_default_relation `{Equiv A} : DefaultRelation () | 3 := {}.
Hint Extern 0 (_ _) => reflexivity : core.
Hint Extern 0 (_ _) => symmetry; assumption : core.
......@@ -396,7 +396,7 @@ Proof. auto. Qed.
(** The classes [PreOrder], [PartialOrder], and [TotalOrder] use an arbitrary
relation [R] instead of [⊆] to support multiple orders on the same type. *)
Definition strict {A} (R : relation A) : relation A := λ X Y, R X Y ¬R Y X.
Instance: Params (@strict) 2.
Instance: Params (@strict) 2 := {}.
Class PartialOrder {A} (R : relation A) : Prop := {
partial_order_pre :> PreOrder R;
partial_order_anti_symm :> AntiSymm (=) R
......@@ -592,9 +592,9 @@ Notation "(, y )" := (λ x, (x,y)) (only parsing) : stdpp_scope.
Notation "p .1" := (fst p) (at level 2, left associativity, format "p .1").
Notation "p .2" := (snd p) (at level 2, left associativity, format "p .2").
Instance: Params (@pair) 2.
Instance: Params (@fst) 2.
Instance: Params (@snd) 2.
Instance: Params (@pair) 2 := {}.
Instance: Params (@fst) 2 := {}.
Instance: Params (@snd) 2 := {}.
Notation curry := prod_curry.
Notation uncurry := prod_uncurry.
......@@ -766,7 +766,7 @@ Instance empty_inhabited `(Empty A) : Inhabited A := populate ∅.
Class Union A := union: A A A.
Hint Mode Union ! : typeclass_instances.
Instance: Params (@union) 2.
Instance: Params (@union) 2 := {}.
Infix "∪" := union (at level 50, left associativity) : stdpp_scope.
Notation "(∪)" := union (only parsing) : stdpp_scope.
Notation "( x ∪)" := (union x) (only parsing) : stdpp_scope.
......@@ -784,7 +784,7 @@ Notation "⋃ l" := (union_list l) (at level 20, format "⋃ l") : stdpp_scope.
Class Intersection A := intersection: A A A.
Hint Mode Intersection ! : typeclass_instances.
Instance: Params (@intersection) 2.
Instance: Params (@intersection) 2 := {}.
Infix "∩" := intersection (at level 40) : stdpp_scope.
Notation "(∩)" := intersection (only parsing) : stdpp_scope.
Notation "( x ∩)" := (intersection x) (only parsing) : stdpp_scope.
......@@ -792,7 +792,7 @@ Notation "(∩ x )" := (λ y, intersection y x) (only parsing) : stdpp_scope.
Class Difference A := difference: A A A.
Hint Mode Difference ! : typeclass_instances.
Instance: Params (@difference) 2.
Instance: Params (@difference) 2 := {}.
Infix "∖" := difference (at level 40, left associativity) : stdpp_scope.
Notation "(∖)" := difference (only parsing) : stdpp_scope.
Notation "( x ∖)" := (difference x) (only parsing) : stdpp_scope.
......@@ -806,7 +806,7 @@ Infix "∖*∖**" := (zip_with (prod_zip (∖) (∖*)))
Class Singleton A B := singleton: A B.
Hint Mode Singleton - ! : typeclass_instances.
Instance: Params (@singleton) 3.
Instance: Params (@singleton) 3 := {}.
Notation "{[ x ]}" := (singleton x) (at level 1) : stdpp_scope.
Notation "{[ x ; y ; .. ; z ]}" :=
(union .. (union (singleton x) (singleton y)) .. (singleton z))
......@@ -818,7 +818,7 @@ Notation "{[ x , y , z ]}" := (singleton (x,y,z))
Class SubsetEq A := subseteq: relation A.
Hint Mode SubsetEq ! : typeclass_instances.
Instance: Params (@subseteq) 2.
Instance: Params (@subseteq) 2 := {}.
Infix "⊆" := subseteq (at level 70) : stdpp_scope.
Notation "(⊆)" := subseteq (only parsing) : stdpp_scope.
Notation "( X ⊆)" := (subseteq X) (only parsing) : stdpp_scope.
......@@ -868,7 +868,7 @@ Hint Mode Lexico ! : typeclass_instances.
Class ElemOf A B := elem_of: A B Prop.
Hint Mode ElemOf - ! : typeclass_instances.
Instance: Params (@elem_of) 3.
Instance: Params (@elem_of) 3 := {}.
Infix "∈" := elem_of (at level 70) : stdpp_scope.
Notation "(∈)" := elem_of (only parsing) : stdpp_scope.
Notation "( x ∈)" := (elem_of x) (only parsing) : stdpp_scope.
......@@ -883,7 +883,7 @@ Notation "(∈@{ B } )" := (@elem_of _ B _) (only parsing) : stdpp_scope.
Class Disjoint A := disjoint : A A Prop.
Hint Mode Disjoint ! : typeclass_instances.
Instance: Params (@disjoint) 2.
Instance: Params (@disjoint) 2 := {}.
Infix "##" := disjoint (at level 70) : stdpp_scope.
Notation "(##)" := disjoint (only parsing) : stdpp_scope.
Notation "( X ##.)" := (disjoint X) (only parsing) : stdpp_scope.
......@@ -904,7 +904,7 @@ Hint Extern 0 (_ ##* _) => symmetry; eassumption : core.
Class DisjointE E A := disjointE : E A A Prop.
Hint Mode DisjointE - ! : typeclass_instances.
Instance: Params (@disjointE) 4.
Instance: Params (@disjointE) 4 := {}.
Notation "X ##{ Γ } Y" := (disjointE Γ X Y)
(at level 70, format "X ##{ Γ } Y") : stdpp_scope.
Notation "(##{ Γ } )" := (disjointE Γ) (only parsing, Γ at level 1) : stdpp_scope.
......@@ -921,7 +921,7 @@ Hint Extern 0 (_ ##{_} _) => symmetry; eassumption : core.
Class DisjointList A := disjoint_list : list A Prop.
Hint Mode DisjointList ! : typeclass_instances.
Instance: Params (@disjoint_list) 2.
Instance: Params (@disjoint_list) 2 := {}.
Notation "## Xs" := (disjoint_list Xs) (at level 20, format "## Xs") : stdpp_scope.
Notation "##@{ A } Xs" :=
(@disjoint_list A _ Xs) (at level 20, only parsing) : stdpp_scope.
......@@ -955,19 +955,19 @@ notations and do not formalize any theory on monads (we do not even define a
class with the monad laws). *)
Class MRet (M : Type Type) := mret: {A}, A M A.
Arguments mret {_ _ _} _ : assert.
Instance: Params (@mret) 3.
Instance: Params (@mret) 3 := {}.
Class MBind (M : Type Type) := mbind : {A B}, (A M B) M A M B.
Arguments mbind {_ _ _ _} _ !_ / : assert.
Instance: Params (@mbind) 4.
Instance: Params (@mbind) 4 := {}.
Class MJoin (M : Type Type) := mjoin: {A}, M (M A) M A.
Arguments mjoin {_ _ _} !_ / : assert.
Instance: Params (@mjoin) 3.
Instance: Params (@mjoin) 3 := {}.
Class FMap (M : Type Type) := fmap : {A B}, (A B) M A M B.
Arguments fmap {_ _ _ _} _ !_ / : assert.
Instance: Params (@fmap) 4.
Instance: Params (@fmap) 4 := {}.
Class OMap (M : Type Type) := omap: {A B}, (A option B) M A M B.
Arguments omap {_ _ _ _} _ !_ / : assert.
Instance: Params (@omap) 4.
Instance: Params (@omap) 4 := {}.
Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : stdpp_scope.
Notation "( m ≫=)" := (λ f, mbind f m) (only parsing) : stdpp_scope.
......@@ -1005,7 +1005,7 @@ on maps. In the file [fin_maps] we will axiomatize finite maps.
The function look up [m !! k] should yield the element at key [k] in [m]. *)
Class Lookup (K A M : Type) := lookup: K M option A.
Hint Mode Lookup - - ! : typeclass_instances.
Instance: Params (@lookup) 4.
Instance: Params (@lookup) 4 := {}.
Notation "m !! i" := (lookup i m) (at level 20) : stdpp_scope.
Notation "(!!)" := lookup (only parsing) : stdpp_scope.
Notation "( m !!)" := (λ i, m !! i) (only parsing) : stdpp_scope.
......@@ -1015,14 +1015,14 @@ Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert.
(** The singleton map *)
Class SingletonM K A M := singletonM: K A M.
Hint Mode SingletonM - - ! : typeclass_instances.
Instance: Params (@singletonM) 5.
Instance: Params (@singletonM) 5 := {}.
Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : stdpp_scope.
(** The function insert [<[k:=a]>m] should update the element at key [k] with
value [a] in [m]. *)
Class Insert (K A M : Type) := insert: K A M M.
Hint Mode Insert - - ! : typeclass_instances.
Instance: Params (@insert) 5.
Instance: Params (@insert) 5 := {}.
Notation "<[ k := a ]>" := (insert k a)
(at level 5, right associativity, format "<[ k := a ]>") : stdpp_scope.
Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
......@@ -1032,14 +1032,14 @@ Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
returned. *)
Class Delete (K M : Type) := delete: K M M.
Hint Mode Delete - ! : typeclass_instances.
Instance: Params (@delete) 4.
Instance: Params (@delete) 4 := {}.
Arguments delete _ _ _ !_ !_ / : simpl nomatch, assert.
(** The function [alter f k m] should update the value at key [k] using the
function [f], which is called with the original value. *)
Class Alter (K A M : Type) := alter: (A A) K M M.
Hint Mode Alter - - ! : typeclass_instances.
Instance: Params (@alter) 5.
Instance: Params (@alter) 5 := {}.
Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert.
(** The function [partial_alter f k m] should update the value at key [k] using the
......@@ -1049,14 +1049,14 @@ yields [None]. *)
Class PartialAlter (K A M : Type) :=
partial_alter: (option A option A) K M M.
Hint Mode PartialAlter - - ! : typeclass_instances.
Instance: Params (@partial_alter) 4.
Instance: Params (@partial_alter) 4 := {}.
Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
(** The function [dom C m] should yield the domain of [m]. That is a finite
collection of type [C] that contains the keys that are a member of [m]. *)
Class Dom (M C : Type) := dom: M C.
Hint Mode Dom ! ! : typeclass_instances.
Instance: Params (@dom) 3.
Instance: Params (@dom) 3 := {}.
Arguments dom : clear implicits.
Arguments dom {_} _ {_} !_ / : simpl nomatch, assert.
......@@ -1065,7 +1065,7 @@ constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)].*)
Class Merge (M : Type Type) :=
merge: {A B C}, (option A option B option C) M A M B M C.
Hint Mode Merge ! : typeclass_instances.
Instance: Params (@merge) 4.
Instance: Params (@merge) 4 := {}.
Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
(** The function [union_with f m1 m2] is supposed to yield the union of [m1]
......@@ -1074,20 +1074,20 @@ both [m1] and [m2]. *)
Class UnionWith (A M : Type) :=
union_with: (A A option A) M M M.
Hint Mode UnionWith - ! : typeclass_instances.
Instance: Params (@union_with) 3.
Instance: Params (@union_with) 3 := {}.
Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
(** Similarly for intersection and difference. *)
Class IntersectionWith (A M : Type) :=
intersection_with: (A A option A) M M M.
Hint Mode IntersectionWith - ! : typeclass_instances.
Instance: Params (@intersection_with) 3.
Instance: Params (@intersection_with) 3 := {}.
Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
Class DifferenceWith (A M : Type) :=
difference_with: (A A option A) M M M.
Hint Mode DifferenceWith - ! : typeclass_instances.
Instance: Params (@difference_with) 3.
Instance: Params (@difference_with) 3 := {}.
Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
Definition intersection_with_list `{IntersectionWith A M}
......@@ -1096,7 +1096,7 @@ Arguments intersection_with_list _ _ _ _ _ !_ / : assert.
Class LookupE (E K A M : Type) := lookupE: E K M option A.
Hint Mode LookupE - - - ! : typeclass_instances.
Instance: Params (@lookupE) 6.
Instance: Params (@lookupE) 6 := {}.
Notation "m !!{ Γ } i" := (lookupE Γ i m)
(at level 20, format "m !!{ Γ } i") : stdpp_scope.
Notation "(!!{ Γ } )" := (lookupE Γ) (only parsing, Γ at level 1) : stdpp_scope.
......@@ -1104,7 +1104,7 @@ Arguments lookupE _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
Class InsertE (E K A M : Type) := insertE: E K A M M.
Hint Mode InsertE - - - ! : typeclass_instances.
Instance: Params (@insertE) 6.
Instance: Params (@insertE) 6 := {}.
Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a)
(at level 5, right associativity, format "<[ k := a ]{ Γ }>") : stdpp_scope.
Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
......@@ -1131,7 +1131,7 @@ enumerated as a list. These elements, given by the [elements] function, may be
in any order and should not contain duplicates. *)
Class Elements A C := elements: C list A.
Hint Mode Elements - ! : typeclass_instances.
Instance: Params (@elements) 3.
Instance: Params (@elements) 3 := {}.
(** We redefine the standard library's [In] and [NoDup] using type classes. *)
Inductive elem_of_list {A} : ElemOf A (list A) :=
......@@ -1168,7 +1168,7 @@ Class FinCollection A C `{ElemOf A C, Empty C, Singleton A C, Union C,
Class Size C := size: C nat.
Hint Mode Size ! : typeclass_instances.
Arguments size {_ _} !_ / : simpl nomatch, assert.
Instance: Params (@size) 2.
Instance: Params (@size) 2 := {}.
(** The class [CollectionMonad M] axiomatizes a type constructor [M] that can be
used to construct a collection [M A] with elements of type [A]. The advantage
......@@ -1195,7 +1195,7 @@ will later prove that [fresh] is [Proper] with respect to the induced setoid
equality on collections. *)
Class Fresh A C := fresh: C A.
Hint Mode Fresh - ! : typeclass_instances.
Instance: Params (@fresh) 3.
Instance: Params (@fresh) 3 := {}.
Class FreshSpec A C `{ElemOf A C,
Empty C, Singleton A C, Union C, Fresh A C} : Prop := {
fresh_collection_simple :>> SimpleCollection A C;
......@@ -1214,7 +1214,7 @@ Notation "½*" := (fmap (M:=list) half) : stdpp_scope.
for the \sqsubseteq symbol. *)
Class SqSubsetEq A := sqsubseteq: relation A.
Hint Mode SqSubsetEq ! : typeclass_instances.
Instance: Params (@sqsubseteq) 2.
Instance: Params (@sqsubseteq) 2 := {}.
Infix "⊑" := sqsubseteq (at level 70) : stdpp_scope.
Notation "(⊑)" := sqsubseteq (only parsing) : stdpp_scope.
Notation "( x ⊑)" := (sqsubseteq x) (only parsing) : stdpp_scope.
......@@ -1223,13 +1223,13 @@ Notation "(⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope.
Infix "⊑@{ A }" := (@sqsubseteq A _) (at level 70, only parsing) : stdpp_scope.
Notation "(⊑@{ A } )" := (@sqsubseteq A _) (only parsing) : stdpp_scope.
Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation ().
Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation () := {}.
Hint Extern 0 (_ _) => reflexivity : core.
Class Meet A := meet: A A A.
Hint Mode Meet ! : typeclass_instances.
Instance: Params (@meet) 2.
Instance: Params (@meet) 2 := {}.
Infix "⊓" := meet (at level 40) : stdpp_scope.
Notation "(⊓)" := meet (only parsing) : stdpp_scope.
Notation "( x ⊓)" := (meet x) (only parsing) : stdpp_scope.
......@@ -1237,7 +1237,7 @@ Notation "(⊓ y )" := (λ x, meet x y) (only parsing) : stdpp_scope.
Class Join A := join: A A A.
Hint Mode Join ! : typeclass_instances.
Instance: Params (@join) 2.
Instance: Params (@join) 2 := {}.
Infix "⊔" := join (at level 50) : stdpp_scope.
Notation "(⊔)" := join (only parsing) : stdpp_scope.
Notation "( x ⊔)" := (join x) (only parsing) : stdpp_scope.
......
......@@ -879,7 +879,7 @@ Fixpoint fresh_list `{Fresh A C, Union C, Singleton A C}
| 0 => []
| S n => let x := fresh X in x :: fresh_list n ({[ x ]} X)
end.
Instance: Params (@fresh_list) 6.
Instance: Params (@fresh_list) 6 := {}.
Inductive Forall_fresh `{ElemOf A C} (X : C) : list A Prop :=
| Forall_fresh_nil : Forall_fresh X []
......@@ -1077,7 +1077,7 @@ End seq_set.
(** Mimimal elements *)
Definition minimal `{ElemOf A C} (R : relation A) (x : A) (X : C) : Prop :=
y, y X R y x R x y.
Instance: Params (@minimal) 5.
Instance: Params (@minimal) 5 := {}.
Typeclasses Opaque minimal.
Section minimal.
......
......@@ -10,9 +10,9 @@ Arguments length {_} _ : assert.
Arguments cons {_} _ _ : assert.
Arguments app {_} _ _ : assert.
Instance: Params (@length) 1.
Instance: Params (@cons) 1.
Instance: Params (@app) 1.
Instance: Params (@length) 1 := {}.
Instance: Params (@cons) 1 := {}.
Instance: Params (@app) 1 := {}.
Notation tail := tl.
Notation take := firstn.
......@@ -22,9 +22,9 @@ Arguments tail {_} _ : assert.
Arguments take {_} !_ !_ / : assert.
Arguments drop {_} !_ !_ / : assert.
Instance: Params (@tail) 1.
Instance: Params (@take) 1.
Instance: Params (@drop) 1.
Instance: Params (@tail) 1 := {}.
Instance: Params (@take) 1 := {}.
Instance: Params (@drop) 1 := {}.
Arguments Permutation {_} _ _ : assert.
Arguments Forall_cons {_} _ _ _ _ _ : assert.
......@@ -90,7 +90,7 @@ Fixpoint list_inserts {A} (i : nat) (k l : list A) : list A :=
| [] => l
| y :: k => <[i:=y]>(list_inserts (S i) k l)
end.
Instance: Params (@list_inserts) 1.
Instance: Params (@list_inserts) 1 := {}.
(** The operation [delete i l] removes the [i]th element of [l] and moves
all consecutive elements one position ahead. In case [i] is out of bounds,
......@@ -105,7 +105,7 @@ Instance list_delete {A} : Delete nat (list A) :=
(** The function [option_list o] converts an element [Some x] into the
singleton list [[x]], and [None] into the empty list [[]]. *)
Definition option_list {A} : option A → list A := option_rect _ (λ x, [x]) [].
Instance: Params (@option_list) 1.
Instance: Params (@option_list) 1 := {}.
Instance maybe_list_singleton {A} : Maybe (λ x : A, [x]) := λ l,
match l with [x] => Some x | _ => None end.
......@@ -126,23 +126,23 @@ Definition list_find {A} P `{∀ x, Decision (P x)} : list A → option (nat * A
| [] => None
| x :: l => if decide (P x) then Some (0,x) else prod_map S id <$> go l
end.
Instance: Params (@list_find) 3.
Instance: Params (@list_find) 3 := {}.
(** The function [replicate n x] generates a list with length [n] of elements
with value [x]. *)
Fixpoint replicate {A} (n : nat) (x : A) : list A :=
match n with 0 => [] | S n => x :: replicate n x end.
Instance: Params (@replicate) 2.
Instance: Params (@replicate) 2 := {}.
(** The function [reverse l] returns the elements of [l] in reverse order. *)
Definition reverse {A} (l : list A) : list A := rev_append l [].
Instance: Params (@reverse) 1.
Instance: Params (@reverse) 1 := {}.
(** The function [last l] returns the last element of the list [l], or [None]
if the list [l] is empty. *)
Fixpoint last {A} (l : list A) : option A :=
match l with [] => None | [x] => Some x | _ :: l => last l end.
Instance: Params (@last) 1.
Instance: Params (@last) 1 := {}.
(** The function [resize n y l] takes the first [n] elements of [l] in case
[length l ≤ n], and otherwise appends elements with value [x] to [l] to obtain
......@@ -153,7 +153,7 @@ Fixpoint resize {A} (n : nat) (y : A) (l : list A) : list A :=
| x :: l => match n with 0 => [] | S n => x :: resize n y l end
end.
Arguments resize {_} !_ _ !_ : assert.
Instance: Params (@resize) 2.
Instance: Params (@resize) 2 := {}.
(** The function [reshape k l] transforms [l] into a list of lists whose sizes
are specified by [k]. In case [l] is too short, the resulting list will be
......@@ -162,7 +162,7 @@ Fixpoint reshape {A} (szs : list nat) (l : list A) : list (list A) :=
match szs with
| [] => [] | sz :: szs => take sz l :: reshape szs (drop sz l)
end.
Instance: Params (@reshape) 2.
Instance: Params (@reshape) 2 := {}.
Definition sublist_lookup {A} (i n : nat) (l : list A) : option (list A) :=
guard (i + n ≤ length l); Some (take n (drop i l)).
......@@ -3603,23 +3603,23 @@ with a binding [i] for [x]. *)
Section quote_lookup.
Context {A : Type}.
Class QuoteLookup (E1 E2 : list A) (x : A) (i : nat) := {}.
Global Instance quote_lookup_here E x : QuoteLookup (x :: E) (x :: E) x 0.
Global Instance quote_lookup_end x : QuoteLookup [] [x] x 0.
Global Instance quote_lookup_here E x : QuoteLookup (x :: E) (x :: E) x 0 := {}.
Global Instance quote_lookup_end x : QuoteLookup [] [x] x 0 := {}.
Global Instance quote_lookup_further E1 E2 x i y :
QuoteLookup E1 E2 x i → QuoteLookup (y :: E1) (y :: E2) x (S i) | 1000.
QuoteLookup E1 E2 x i → QuoteLookup (y :: E1) (y :: E2) x (S i) | 1000 := {}.
End quote_lookup.
Section quote.
Context {A : Type}.
Class Quote (E1 E2 : env A) (l : list A) (t : rlist nat) := {}.
Global Instance quote_nil: Quote E1 E1 [] rnil.
Global Instance quote_nil: Quote E1 E1 [] rnil := {}.
Global Instance quote_node E1 E2 l i:
QuoteLookup E1 E2 l i → Quote E1 E2 l (rnode i) | 1000.
QuoteLookup E1 E2 l i → Quote E1 E2 l (rnode i) | 1000 := {}.
Global Instance quote_cons E1 E2 E3 x l i t :
QuoteLookup E1 E2 [x] i →
Quote E2 E3 l t → Quote E1 E3 (x :: l) (rapp (rnode i) t).
Quote E2 E3 l t → Quote E1 E3 (x :: l) (rapp (rnode i) t) := {}.
Global Instance quote_app E1 E2 E3 l1 l2 t1 t2 :
Quote E1 E2 l1 t1 → Quote E2 E3 l2 t2 → Quote E1 E3 (l1 ++ l2) (rapp t1 t2).
Quote E1 E2 l1 t1 → Quote E2 E3 l2 t2 → Quote E1 E3 (l1 ++ l2) (rapp t1 t2) := {}.
End quote.
Section eval.
......
......@@ -23,7 +23,7 @@ Proof. congruence. Qed.
(** The [from_option] is the eliminator for option. *)
Definition from_option {A B} (f : A B) (y : B) (mx : option A) : B :=
match mx with None => y | Some x => f x end.
Instance: Params (@from_option) 3.
Instance: Params (@from_option) 3 := {}.
Arguments from_option {_ _} _ _ !_ / : assert.
(** The eliminator with the identity function. *)
......@@ -40,7 +40,7 @@ Lemma option_eq_1_alt {A} (mx my : option A) x :
Proof. congruence. Qed.
Definition is_Some {A} (mx : option A) := x, mx = Some x.
Instance: Params (@is_Some) 1.
Instance: Params (@is_Some) 1 := {}.
Lemma is_Some_alt {A} (mx : option A) :
is_Some mx match mx with Some _ => True | None => False end.
......
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