rfl に名前の由来を追加

lean-ja · Sep 22, 2023 · f46e43c · f46e43c
1 parent ac33d70
commit f46e43c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/rfl.md b/src/rfl.md
@@ -1,6 +1,6 @@
 # rfl
 
-`rfl` は，定義から等しいものが等しいことを示すタクティクです．
+`rfl` は，定義から等しいものが等しいことを示すタクティクです．反射律(reflexivity)からその名前があります．
 
 ```lean
 {{#include ../Examples/Rfl.lean}}