golb erutufAgda2 | 01:32Agda2 はタクティクスがないのでちょっとしたことを証明するのも面倒になることがしばしば。そこで推移律でずらずら並べるだけの証明をしたいとき便利なのが standard library の Relation.Binary.PreorderReasoning。そして standard library 持ち出すまでもないちょっとした証明用にほとんど一緒だけど自分で書いてみる。イコール専用。 infixr 6 _==_ _==_ : forall {A : Set} -> A -> A -> Set1 a == b = (P : _ -> Set) -> P a -> P b eqrefl : forall {A : Set} {x : A} -> x == x eqrefl _ p = p eqtrans : forall {A : Set} {n m l : A}
